Theorem exbiri 823

Description: Inference form of exbir 45421. This proof is exbiriVD 45795 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  5370  ralxfrd2  5374  tfrlem9  8377  tz7.48lem  8434  mapfset  8856  sbthlem1  9090  addcanpr  11112  axpre-sup  11235  lbreu  12248  zmax  13053  uzsubsubfz  13660  elfzodifsumelfzo  13846  pfxccatin12lem3  14861  cshwidxmod  14934  prmgaplem6  17214  ucnima  24579  gausslemma2dlem1a  27674  usgredg2vlem2  29789  umgr2v2enb1  30089  wwlksnext  30464  wwlksnextwrd  30468  clwwlkccatlem  30562  mdslmd1lem1  32909  mdslmd1lem2  32910  dfon2  36524  cgrextend  36743  brsegle  36843  finxpsuclem  38288  poimirlem18  38524  poimirlem21  38527  brabg2  38619  dfatcolem  48269  iccelpart  48459