Theorem exbiri 810

Description: Inference form of exbir 41184. This proof is exbiriVD 41560 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 481	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜒)
3	2	exp31 423	1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  biimp3ar  1467  ralxfrd  5274  ralxfrd2  5278  tfrlem9  8004  sbthlem1  8611  addcanpr  10457  axpre-sup  10580  lbreu  11578  zmax  12333  uzsubsubfz  12924  elfzodifsumelfzo  13098  pfxccatin12lem3  14085  cshwidxmod  14156  prmgaplem6  16382  ucnima  22887  gausslemma2dlem1a  25949  usgredg2vlem2  27016  umgr2v2enb1  27316  wwlksnext  27679  wwlksnextwrd  27683  clwwlkccatlem  27774  mdslmd1lem1  30108  mdslmd1lem2  30109  dfon2  33150  cgrextend  33582  brsegle  33682  finxpsuclem  34814  poimirlem18  35075  poimirlem21  35078  brabg2  35154  dfatcolem  43811  iccelpart  43950