Theorem exbiri 810

Description: Inference form of exbir 44449. This proof is exbiriVD 44825 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  1470  ralxfrd  5426  ralxfrd2  5430  tfrlem9  8441  mapfset  8908  sbthlem1  9149  addcanpr  11115  axpre-sup  11238  lbreu  12245  zmax  13010  uzsubsubfz  13606  elfzodifsumelfzo  13782  pfxccatin12lem3  14780  cshwidxmod  14851  prmgaplem6  17103  ucnima  24311  gausslemma2dlem1a  27427  usgredg2vlem2  29261  umgr2v2enb1  29562  wwlksnext  29926  wwlksnextwrd  29930  clwwlkccatlem  30021  mdslmd1lem1  32357  mdslmd1lem2  32358  dfon2  35756  cgrextend  35972  brsegle  36072  finxpsuclem  37363  poimirlem18  37598  poimirlem21  37601  brabg2  37677  dfatcolem  47170  iccelpart  47307