Theorem exbiri 808

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.)

Hypothesis

Ref	Expression
exbiri.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
exbiri	⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

Proof of Theorem exbiri

Step	Hyp	Ref	Expression
1		exbiri.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
2	1	biimpar 478	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜒)
3	2	exp31 420	1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

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