Theorem exbiri 823

Description: Inference form of exbir 45304. This proof is exbiriVD 45678 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  1499  ralxfrd  5377  ralxfrd2  5381  tfrlem9  8377  mapfset  8854  sbthlem1  9088  addcanpr  11058  axpre-sup  11181  lbreu  12192  zmax  12997  uzsubsubfz  13603  elfzodifsumelfzo  13789  pfxccatin12lem3  14803  cshwidxmod  14876  prmgaplem6  17152  ucnima  24510  gausslemma2dlem1a  27602  usgredg2vlem2  29687  umgr2v2enb1  29987  wwlksnext  30362  wwlksnextwrd  30366  clwwlkccatlem  30460  mdslmd1lem1  32807  mdslmd1lem2  32808  dfon2  36371  cgrextend  36590  brsegle  36690  finxpsuclem  38153  poimirlem18  38389  poimirlem21  38392  brabg2  38469  dfatcolem  48145  iccelpart  48335