Theorem exbiri 816

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  biimp3ar  1478  ralxfrd  5344  ralxfrd2  5348  tfrlem9  8321  mapfset  8794  sbthlem1  9022  addcanpr  10967  axpre-sup  11090  lbreu  12104  zmax  12893  uzsubsubfz  13498  elfzodifsumelfzo  13684  pfxccatin12lem3  14692  cshwidxmod  14763  prmgaplem6  17025  ucnima  24270  gausslemma2dlem1a  27353  usgredg2vlem2  29320  umgr2v2enb1  29620  wwlksnext  29986  wwlksnextwrd  29990  clwwlkccatlem  30084  mdslmd1lem1  32421  mdslmd1lem2  32422  dfon2  36025  cgrextend  36243  brsegle  36343  finxpsuclem  37766  poimirlem18  38012  poimirlem21  38015  brabg2  38091  dfatcolem  47725  iccelpart  47915