Theorem exbiri 653

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  biimp3ar  1570  ralxfrd  5016  ralxfrd2  5021  tfrlem9  7638  sbthlem1  8223  addcanpr  10031  axpre-sup  10153  lbreu  11136  zmax  11949  uzsubsubfz  12527  elfzodifsumelfzo  12699  swrdccatin12lem3  13661  cshwidxmod  13720  prmgaplem6  15933  ucnima  22257  gausslemma2dlem1a  25260  usgredg2vlem2  26288  umgr2v2enb1  26603  wwlksnextwrd  26986  mdslmd1lem1  29464  mdslmd1lem2  29465  dfon2  31973  cgrextend  32392  brsegle  32492  finxpsuclem  33516  poimirlem18  33709  poimirlem21  33712  brabg2  33792  iccelpart  41848