Theorem exbiri 811

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  biimp3ar  1471  ralxfrd  5275  ralxfrd2  5279  tfrlem9  8050  mapfset  8460  sbthlem1  8677  addcanpr  10546  axpre-sup  10669  lbreu  11668  zmax  12427  uzsubsubfz  13020  elfzodifsumelfzo  13194  pfxccatin12lem3  14183  cshwidxmod  14254  prmgaplem6  16492  ucnima  23033  gausslemma2dlem1a  26101  usgredg2vlem2  27168  umgr2v2enb1  27468  wwlksnext  27831  wwlksnextwrd  27835  clwwlkccatlem  27926  mdslmd1lem1  30260  mdslmd1lem2  30261  dfon2  33340  cgrextend  33948  brsegle  34048  finxpsuclem  35191  poimirlem18  35418  poimirlem21  35421  brabg2  35497  dfatcolem  44280  iccelpart  44419