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 38684. This proof is exbiriVD 39089 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 502 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜒) |
3 | 2 | exp31 630 | 1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 |
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 197 df-an 386 |
This theorem is referenced by: biimp3ar 1433 ralxfrd 4879 ralxfrd2 4884 tfrlem9 7481 sbthlem1 8070 addcanpr 9868 axpre-sup 9990 lbreu 10973 zmax 11785 uzsubsubfz 12363 elfzodifsumelfzo 12533 swrdccatin12lem3 13490 cshwidxmod 13549 prmgaplem6 15760 ucnima 22085 gausslemma2dlem1a 25090 usgredg2vlem2 26118 umgr2v2enb1 26422 wwlksnextwrd 26792 numclwlk1lem2f1 27227 mdslmd1lem1 29184 mdslmd1lem2 29185 dfon2 31697 cgrextend 32115 brsegle 32215 finxpsuclem 33234 poimirlem18 33427 poimirlem21 33430 brabg2 33510 iccelpart 41369 |
Copyright terms: Public domain | W3C validator |