Theorem exbiri 822

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

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

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 401

This theorem is referenced by:  biimp3ar  1499  ralxfrd  5381  ralxfrd2  5385  tfrlem9  8373  mapfset  8848  sbthlem1  9076  addcanpr  11032  axpre-sup  11155  lbreu  12166  zmax  12970  uzsubsubfz  13576  elfzodifsumelfzo  13762  pfxccatin12lem3  14771  cshwidxmod  14842  prmgaplem6  17117  ucnima  24418  gausslemma2dlem1a  27507  usgredg2vlem2  29554  umgr2v2enb1  29854  wwlksnext  30220  wwlksnextwrd  30224  clwwlkccatlem  30318  mdslmd1lem1  32655  mdslmd1lem2  32656  dfon2  36260  cgrextend  36478  brsegle  36578  finxpsuclem  38021  poimirlem18  38267  poimirlem21  38270  brabg2  38346  dfatcolem  47969  iccelpart  48159