Theorem exbiri 810

Description: Inference form of exbir 44511. This proof is exbiriVD 44885 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  5346  ralxfrd2  5350  tfrlem9  8304  mapfset  8774  sbthlem1  9000  addcanpr  10934  axpre-sup  11057  lbreu  12069  zmax  12840  uzsubsubfz  13443  elfzodifsumelfzo  13628  pfxccatin12lem3  14636  cshwidxmod  14707  prmgaplem6  16965  ucnima  24193  gausslemma2dlem1a  27301  usgredg2vlem2  29202  umgr2v2enb1  29503  wwlksnext  29869  wwlksnextwrd  29873  clwwlkccatlem  29964  mdslmd1lem1  32300  mdslmd1lem2  32301  dfon2  35825  cgrextend  36041  brsegle  36141  finxpsuclem  37430  poimirlem18  37677  poimirlem21  37680  brabg2  37756  dfatcolem  47285  iccelpart  47463