Theorem exbiri 846

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

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

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 386

This theorem is referenced by:  biimp3ar  1595  ralxfrd  5078  ralxfrd2  5082  tfrlem9  7720  sbthlem1  8312  addcanpr  10156  axpre-sup  10278  lbreu  11265  zmax  12030  uzsubsubfz  12617  elfzodifsumelfzo  12789  swrdccatin12lem3  13794  cshwidxmod  13888  prmgaplem6  16093  ucnima  22413  gausslemma2dlem1a  25442  usgredg2vlem2  26459  umgr2v2enb1  26776  wwlksnextwrd  27169  wwlksnextwrdOLD  27174  mdslmd1lem1  29709  mdslmd1lem2  29710  dfon2  32209  cgrextend  32628  brsegle  32728  finxpsuclem  33732  poimirlem18  33916  poimirlem21  33919  brabg2  33998  dfatcolem  42109  iccelpart  42209