Theorem exbiri 822

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  biimp3ar  1494  ralxfrd  5370  ralxfrd2  5374  tfrlem9  8360  mapfset  8835  sbthlem1  9063  addcanpr  11019  axpre-sup  11142  lbreu  12156  zmax  12960  uzsubsubfz  13565  elfzodifsumelfzo  13751  pfxccatin12lem3  14759  cshwidxmod  14830  prmgaplem6  17106  ucnima  24398  gausslemma2dlem1a  27487  usgredg2vlem2  29485  umgr2v2enb1  29785  wwlksnext  30151  wwlksnextwrd  30155  clwwlkccatlem  30249  mdslmd1lem1  32586  mdslmd1lem2  32587  dfon2  36153  cgrextend  36371  brsegle  36471  finxpsuclem  37903  poimirlem18  38149  poimirlem21  38152  brabg2  38228  dfatcolem  47847  iccelpart  48037