Theorem exbiri 810

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  biimp3ar  1472  ralxfrd  5353  ralxfrd2  5357  tfrlem9  8316  mapfset  8787  sbthlem1  9015  addcanpr  10957  axpre-sup  11080  lbreu  12092  zmax  12858  uzsubsubfz  13462  elfzodifsumelfzo  13647  pfxccatin12lem3  14655  cshwidxmod  14726  prmgaplem6  16984  ucnima  24224  gausslemma2dlem1a  27332  usgredg2vlem2  29299  umgr2v2enb1  29600  wwlksnext  29966  wwlksnextwrd  29970  clwwlkccatlem  30064  mdslmd1lem1  32400  mdslmd1lem2  32401  dfon2  35984  cgrextend  36202  brsegle  36302  finxpsuclem  37598  poimirlem18  37835  poimirlem21  37838  brabg2  37914  dfatcolem  47497  iccelpart  47675