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 40832. This proof is exbiriVD 41208 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 480 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜒) |
3 | 2 | exp31 422 | 1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: biimp3ar 1466 ralxfrd 5309 ralxfrd2 5313 tfrlem9 8021 sbthlem1 8627 addcanpr 10468 axpre-sup 10591 lbreu 11591 zmax 12346 uzsubsubfz 12930 elfzodifsumelfzo 13104 pfxccatin12lem3 14094 cshwidxmod 14165 prmgaplem6 16392 ucnima 22890 gausslemma2dlem1a 25941 usgredg2vlem2 27008 umgr2v2enb1 27308 wwlksnext 27671 wwlksnextwrd 27675 clwwlkccatlem 27767 mdslmd1lem1 30102 mdslmd1lem2 30103 dfon2 33037 cgrextend 33469 brsegle 33569 finxpsuclem 34681 poimirlem18 34925 poimirlem21 34928 brabg2 35006 dfatcolem 43474 iccelpart 43613 |
Copyright terms: Public domain | W3C validator |