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 42098. This proof is exbiriVD 42474 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 478 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜒) |
3 | 2 | exp31 420 | 1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 |
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 397 |
This theorem is referenced by: biimp3ar 1469 ralxfrd 5331 ralxfrd2 5335 tfrlem9 8216 mapfset 8638 sbthlem1 8870 addcanpr 10802 axpre-sup 10925 lbreu 11925 zmax 12685 uzsubsubfz 13278 elfzodifsumelfzo 13453 pfxccatin12lem3 14445 cshwidxmod 14516 prmgaplem6 16757 ucnima 23433 gausslemma2dlem1a 26513 usgredg2vlem2 27593 umgr2v2enb1 27893 wwlksnext 28258 wwlksnextwrd 28262 clwwlkccatlem 28353 mdslmd1lem1 30687 mdslmd1lem2 30688 dfon2 33768 cgrextend 34310 brsegle 34410 finxpsuclem 35568 poimirlem18 35795 poimirlem21 35798 brabg2 35874 dfatcolem 44747 iccelpart 44885 |
Copyright terms: Public domain | W3C validator |