Theorem exbiri 845

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  biimp3ar  1598  ralxfrd  5108  ralxfrd2  5112  tfrlem9  7747  sbthlem1  8339  addcanpr  10183  axpre-sup  10306  lbreu  11303  zmax  12068  uzsubsubfz  12656  elfzodifsumelfzo  12829  swrdccatin12lem3  13830  cshwidxmod  13924  prmgaplem6  16131  ucnima  22455  gausslemma2dlem1a  25503  usgredg2vlem2  26522  umgr2v2enb1  26824  wwlksnextwrd  27211  wwlksnextwrdOLD  27216  mdslmd1lem1  29728  mdslmd1lem2  29729  dfon2  32224  cgrextend  32643  brsegle  32743  finxpsuclem  33772  poimirlem18  33964  poimirlem21  33967  brabg2  34046  dfatcolem  42150  iccelpart  42250