Theorem exbiri 820

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  biimp3ar  1490  ralxfrd  5364  ralxfrd2  5368  tfrlem9  8351  mapfset  8827  sbthlem1  9055  addcanpr  11001  axpre-sup  11124  lbreu  12139  zmax  12943  uzsubsubfz  13548  elfzodifsumelfzo  13734  pfxccatin12lem3  14742  cshwidxmod  14813  prmgaplem6  17075  ucnima  24320  gausslemma2dlem1a  27406  usgredg2vlem2  29373  umgr2v2enb1  29673  wwlksnext  30039  wwlksnextwrd  30043  clwwlkccatlem  30137  mdslmd1lem1  32474  mdslmd1lem2  32475  dfon2  36104  cgrextend  36322  brsegle  36422  finxpsuclem  37855  poimirlem18  38101  poimirlem21  38104  brabg2  38180  dfatcolem  47813  iccelpart  48003