Theorem exbiri 823

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  biimp3ar  1499  ralxfrd  5377  ralxfrd2  5381  tfrlem9  8378  mapfset  8855  sbthlem1  9089  addcanpr  11059  axpre-sup  11182  lbreu  12193  zmax  12998  uzsubsubfz  13605  elfzodifsumelfzo  13791  pfxccatin12lem3  14805  cshwidxmod  14878  prmgaplem6  17154  ucnima  24512  gausslemma2dlem1a  27609  usgredg2vlem2  29694  umgr2v2enb1  29994  wwlksnext  30369  wwlksnextwrd  30373  clwwlkccatlem  30467  mdslmd1lem1  32814  mdslmd1lem2  32815  dfon2  36377  cgrextend  36596  brsegle  36696  finxpsuclem  38159  poimirlem18  38395  poimirlem21  38398  brabg2  38475  dfatcolem  48151  iccelpart  48341