Theorem exbiri 809

Description: Inference form of exbir 43541. This proof is exbiriVD 43917 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  1470  ralxfrd  5406  ralxfrd2  5410  tfrlem9  8387  mapfset  8846  sbthlem1  9085  addcanpr  11043  axpre-sup  11166  lbreu  12168  zmax  12933  uzsubsubfz  13527  elfzodifsumelfzo  13702  pfxccatin12lem3  14686  cshwidxmod  14757  prmgaplem6  16993  ucnima  24006  gausslemma2dlem1a  27092  usgredg2vlem2  28738  umgr2v2enb1  29038  wwlksnext  29402  wwlksnextwrd  29406  clwwlkccatlem  29497  mdslmd1lem1  31833  mdslmd1lem2  31834  dfon2  35056  cgrextend  35272  brsegle  35372  finxpsuclem  36581  poimirlem18  36809  poimirlem21  36812  brabg2  36888  dfatcolem  46262  iccelpart  46400