Theorem exbiri 811

Description: Inference form of exbir 44476. This proof is exbiriVD 44852 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  1469  ralxfrd  5414  ralxfrd2  5418  tfrlem9  8424  mapfset  8889  sbthlem1  9122  addcanpr  11084  axpre-sup  11207  lbreu  12216  zmax  12985  uzsubsubfz  13583  elfzodifsumelfzo  13767  pfxccatin12lem3  14767  cshwidxmod  14838  prmgaplem6  17090  ucnima  24306  gausslemma2dlem1a  27424  usgredg2vlem2  29258  umgr2v2enb1  29559  wwlksnext  29923  wwlksnextwrd  29927  clwwlkccatlem  30018  mdslmd1lem1  32354  mdslmd1lem2  32355  dfon2  35774  cgrextend  35990  brsegle  36090  finxpsuclem  37380  poimirlem18  37625  poimirlem21  37628  brabg2  37704  dfatcolem  47205  iccelpart  47358