Theorem exbiri 810

Description: Inference form of exbir 44596. This proof is exbiriVD 44970 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  5348  ralxfrd2  5352  tfrlem9  8310  mapfset  8780  sbthlem1  9007  addcanpr  10944  axpre-sup  11067  lbreu  12079  zmax  12845  uzsubsubfz  13448  elfzodifsumelfzo  13633  pfxccatin12lem3  14641  cshwidxmod  14712  prmgaplem6  16970  ucnima  24196  gausslemma2dlem1a  27304  usgredg2vlem2  29206  umgr2v2enb1  29507  wwlksnext  29873  wwlksnextwrd  29877  clwwlkccatlem  29971  mdslmd1lem1  32307  mdslmd1lem2  32308  dfon2  35855  cgrextend  36073  brsegle  36173  finxpsuclem  37462  poimirlem18  37698  poimirlem21  37701  brabg2  37777  dfatcolem  47379  iccelpart  47557