Theorem exbiri 809

Description: Inference form of exbir 42882. This proof is exbiriVD 43258 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 205   ∧ 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 206  df-an 397

This theorem is referenced by:  biimp3ar  1470  ralxfrd  5368  ralxfrd2  5372  tfrlem9  8336  mapfset  8795  sbthlem1  9034  addcanpr  10991  axpre-sup  11114  lbreu  12114  zmax  12879  uzsubsubfz  13473  elfzodifsumelfzo  13648  pfxccatin12lem3  14632  cshwidxmod  14703  prmgaplem6  16939  ucnima  23670  gausslemma2dlem1a  26750  usgredg2vlem2  28237  umgr2v2enb1  28537  wwlksnext  28901  wwlksnextwrd  28905  clwwlkccatlem  28996  mdslmd1lem1  31330  mdslmd1lem2  31331  dfon2  34453  cgrextend  34669  brsegle  34769  finxpsuclem  35941  poimirlem18  36169  poimirlem21  36172  brabg2  36248  dfatcolem  45607  iccelpart  45745