![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exbiri | Structured version Visualization version GIF version |
Description: Inference form of exbir 39155. This proof is exbiriVD 39557 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.) |
Ref | Expression |
---|---|
exbiri.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
exbiri | ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exbiri.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | |
2 | 1 | biimpar 503 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜒) |
3 | 2 | exp31 631 | 1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 385 |
This theorem is referenced by: biimp3ar 1570 ralxfrd 5016 ralxfrd2 5021 tfrlem9 7638 sbthlem1 8223 addcanpr 10031 axpre-sup 10153 lbreu 11136 zmax 11949 uzsubsubfz 12527 elfzodifsumelfzo 12699 swrdccatin12lem3 13661 cshwidxmod 13720 prmgaplem6 15933 ucnima 22257 gausslemma2dlem1a 25260 usgredg2vlem2 26288 umgr2v2enb1 26603 wwlksnextwrd 26986 mdslmd1lem1 29464 mdslmd1lem2 29465 dfon2 31973 cgrextend 32392 brsegle 32492 finxpsuclem 33516 poimirlem18 33709 poimirlem21 33712 brabg2 33792 iccelpart 41848 |
Copyright terms: Public domain | W3C validator |