![]() |
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 43110. This proof is exbiriVD 43486 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 479 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜒) |
3 | 2 | exp31 421 | 1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: biimp3ar 1471 ralxfrd 5402 ralxfrd2 5406 tfrlem9 8372 mapfset 8832 sbthlem1 9071 addcanpr 11028 axpre-sup 11151 lbreu 12151 zmax 12916 uzsubsubfz 13510 elfzodifsumelfzo 13685 pfxccatin12lem3 14669 cshwidxmod 14740 prmgaplem6 16976 ucnima 23755 gausslemma2dlem1a 26835 usgredg2vlem2 28450 umgr2v2enb1 28750 wwlksnext 29114 wwlksnextwrd 29118 clwwlkccatlem 29209 mdslmd1lem1 31543 mdslmd1lem2 31544 dfon2 34695 cgrextend 34911 brsegle 35011 finxpsuclem 36183 poimirlem18 36411 poimirlem21 36414 brabg2 36490 dfatcolem 45836 iccelpart 45974 |
Copyright terms: Public domain | W3C validator |