Theorem exbiri 810

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  biimp3ar  1472  ralxfrd  5366  ralxfrd2  5370  tfrlem9  8356  mapfset  8826  sbthlem1  9057  addcanpr  11006  axpre-sup  11129  lbreu  12140  zmax  12911  uzsubsubfz  13514  elfzodifsumelfzo  13699  pfxccatin12lem3  14704  cshwidxmod  14775  prmgaplem6  17034  ucnima  24175  gausslemma2dlem1a  27283  usgredg2vlem2  29160  umgr2v2enb1  29461  wwlksnext  29830  wwlksnextwrd  29834  clwwlkccatlem  29925  mdslmd1lem1  32261  mdslmd1lem2  32262  dfon2  35787  cgrextend  36003  brsegle  36103  finxpsuclem  37392  poimirlem18  37639  poimirlem21  37642  brabg2  37718  dfatcolem  47260  iccelpart  47438