Theorem exbiri 823

Description: Inference form of exbir 45229. This proof is exbiriVD 45603 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  5384  ralxfrd2  5388  tfrlem9  8381  mapfset  8856  sbthlem1  9085  addcanpr  11049  axpre-sup  11172  lbreu  12183  zmax  12987  uzsubsubfz  13593  elfzodifsumelfzo  13779  pfxccatin12lem3  14793  cshwidxmod  14866  prmgaplem6  17141  ucnima  24474  gausslemma2dlem1a  27566  usgredg2vlem2  29613  umgr2v2enb1  29913  wwlksnext  30279  wwlksnextwrd  30283  clwwlkccatlem  30377  mdslmd1lem1  32714  mdslmd1lem2  32715  dfon2  36303  cgrextend  36521  brsegle  36621  finxpsuclem  38084  poimirlem18  38330  poimirlem21  38333  brabg2  38409  dfatcolem  48033  iccelpart  48223