Theorem exbiri 823

Description: Inference form of exbir 45555. This proof is exbiriVD 45929 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  5369  ralxfrd2  5373  tfrlem9  8396  tz7.48lem  8453  mapfset  8875  sbthlem1  9109  addcanpr  11134  axpre-sup  11257  lbreu  12270  zmax  13075  uzsubsubfz  13683  elfzodifsumelfzo  13869  pfxccatin12lem3  14885  cshwidxmod  14958  prmgaplem6  17239  ucnima  24604  gausslemma2dlem1a  27697  usgredg2vlem2  29812  umgr2v2enb1  30112  wwlksnext  30487  wwlksnextwrd  30491  clwwlkccatlem  30585  mdslmd1lem1  32932  mdslmd1lem2  32933  dfon2  36646  cgrextend  36865  brsegle  36965  finxpsuclem  38413  poimirlem18  38649  poimirlem21  38652  brabg2  38744  dfatcolem  48418  iccelpart  48608