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 41636. This proof is exbiriVD 42012 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 481 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜒) |
3 | 2 | exp31 423 | 1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: biimp3ar 1471 ralxfrd 5275 ralxfrd2 5279 tfrlem9 8050 mapfset 8460 sbthlem1 8677 addcanpr 10546 axpre-sup 10669 lbreu 11668 zmax 12427 uzsubsubfz 13020 elfzodifsumelfzo 13194 pfxccatin12lem3 14183 cshwidxmod 14254 prmgaplem6 16492 ucnima 23033 gausslemma2dlem1a 26101 usgredg2vlem2 27168 umgr2v2enb1 27468 wwlksnext 27831 wwlksnextwrd 27835 clwwlkccatlem 27926 mdslmd1lem1 30260 mdslmd1lem2 30261 dfon2 33340 cgrextend 33948 brsegle 34048 finxpsuclem 35191 poimirlem18 35418 poimirlem21 35421 brabg2 35497 dfatcolem 44280 iccelpart 44419 |
Copyright terms: Public domain | W3C validator |