Theorem exbiri 810

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  biimp3ar  1472  ralxfrd  5363  ralxfrd2  5367  tfrlem9  8353  mapfset  8823  sbthlem1  9051  addcanpr  10999  axpre-sup  11122  lbreu  12133  zmax  12904  uzsubsubfz  13507  elfzodifsumelfzo  13692  pfxccatin12lem3  14697  cshwidxmod  14768  prmgaplem6  17027  ucnima  24168  gausslemma2dlem1a  27276  usgredg2vlem2  29153  umgr2v2enb1  29454  wwlksnext  29823  wwlksnextwrd  29827  clwwlkccatlem  29918  mdslmd1lem1  32254  mdslmd1lem2  32255  dfon2  35780  cgrextend  35996  brsegle  36096  finxpsuclem  37385  poimirlem18  37632  poimirlem21  37635  brabg2  37711  dfatcolem  47256  iccelpart  47434