![]() |
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 39515. This proof is exbiriVD 39901 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 471 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜒) |
3 | 2 | exp31 412 | 1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: biimp3ar 1598 ralxfrd 5108 ralxfrd2 5112 tfrlem9 7747 sbthlem1 8339 addcanpr 10183 axpre-sup 10306 lbreu 11303 zmax 12068 uzsubsubfz 12656 elfzodifsumelfzo 12829 swrdccatin12lem3 13830 cshwidxmod 13924 prmgaplem6 16131 ucnima 22455 gausslemma2dlem1a 25503 usgredg2vlem2 26522 umgr2v2enb1 26824 wwlksnextwrd 27211 wwlksnextwrdOLD 27216 mdslmd1lem1 29728 mdslmd1lem2 29729 dfon2 32224 cgrextend 32643 brsegle 32743 finxpsuclem 33772 poimirlem18 33964 poimirlem21 33967 brabg2 34046 dfatcolem 42150 iccelpart 42250 |
Copyright terms: Public domain | W3C validator |