![]() |
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 39464. This proof is exbiriVD 39850 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 470 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜒) |
3 | 2 | exp31 411 | 1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 385 |
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 386 |
This theorem is referenced by: biimp3ar 1595 ralxfrd 5078 ralxfrd2 5082 tfrlem9 7720 sbthlem1 8312 addcanpr 10156 axpre-sup 10278 lbreu 11265 zmax 12030 uzsubsubfz 12617 elfzodifsumelfzo 12789 swrdccatin12lem3 13794 cshwidxmod 13888 prmgaplem6 16093 ucnima 22413 gausslemma2dlem1a 25442 usgredg2vlem2 26459 umgr2v2enb1 26776 wwlksnextwrd 27169 wwlksnextwrdOLD 27174 mdslmd1lem1 29709 mdslmd1lem2 29710 dfon2 32209 cgrextend 32628 brsegle 32728 finxpsuclem 33732 poimirlem18 33916 poimirlem21 33919 brabg2 33998 dfatcolem 42109 iccelpart 42209 |
Copyright terms: Public domain | W3C validator |