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 37705. This proof is exbiriVD 38111 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 501 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜒) |
3 | 2 | exp31 628 | 1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: biimp3ar 1425 ralxfrd 4805 ralxfrd2 4810 tfrlem9 7368 sbthlem1 7955 addcanpr 9747 axpre-sup 9869 lbreu 10852 zmax 11661 uzsubsubfz 12234 elfzodifsumelfzo 12401 swrdccatin12lem3 13341 cshwidxmod 13400 prmgaplem6 15598 ucnima 21895 gausslemma2dlem1a 24890 usgraidx2vlem2 25921 wwlkextwrd 26256 numclwlk1lem2f1 26621 mdslmd1lem1 28568 mdslmd1lem2 28569 dfon2 30941 cgrextend 31285 brsegle 31385 finxpsuclem 32410 poimirlem18 32597 poimirlem21 32600 brabg2 32680 iccelpart 39971 usgredg2vlem2 40453 umgr2v2enb1 40742 wwlksnextwrd 41103 av-numclwlk1lem2f1 41524 |
Copyright terms: Public domain | W3C validator |