Theorem exbiri 823

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  biimp3ar  1500  ralxfrd  5374  ralxfrd2  5378  tfrlem9  8421  tz7.48lem  8478  mapfset  8900  sbthlem1  9134  addcanpr  11158  axpre-sup  11281  lbreu  12294  zmax  13099  uzsubsubfz  13707  elfzodifsumelfzo  13893  pfxccatin12lem3  14909  cshwidxmod  14982  prmgaplem6  17263  ucnima  24629  gausslemma2dlem1a  27722  usgredg2vlem2  29837  umgr2v2enb1  30137  wwlksnext  30512  wwlksnextwrd  30516  clwwlkccatlem  30610  mdslmd1lem1  32957  mdslmd1lem2  32958  dfon2  36732  cgrextend  36951  brsegle  37051  finxpsuclem  38512  poimirlem18  38748  poimirlem21  38751  brabg2  38843  dfatcolem  48530  iccelpart  48720