Theorem exbiri 651

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

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

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 386

This theorem is referenced by:  biimp3ar  1430  ralxfrd  4849  ralxfrd2  4854  tfrlem9  7441  sbthlem1  8030  addcanpr  9828  axpre-sup  9950  lbreu  10933  zmax  11745  uzsubsubfz  12321  elfzodifsumelfzo  12490  swrdccatin12lem3  13443  cshwidxmod  13502  prmgaplem6  15703  ucnima  22025  gausslemma2dlem1a  25024  usgredg2vlem2  26045  umgr2v2enb1  26342  wwlksnextwrd  26695  numclwlk1lem2f1  27116  mdslmd1lem1  29072  mdslmd1lem2  29073  dfon2  31451  cgrextend  31810  brsegle  31910  finxpsuclem  32905  poimirlem18  33098  poimirlem21  33101  brabg2  33181  iccelpart  40697