Theorem exbiri 810

Description: Inference form of exbir 44453. This proof is exbiriVD 44827 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  5350  ralxfrd2  5354  tfrlem9  8314  mapfset  8784  sbthlem1  9011  addcanpr  10959  axpre-sup  11082  lbreu  12093  zmax  12864  uzsubsubfz  13467  elfzodifsumelfzo  13652  pfxccatin12lem3  14656  cshwidxmod  14727  prmgaplem6  16986  ucnima  24184  gausslemma2dlem1a  27292  usgredg2vlem2  29189  umgr2v2enb1  29490  wwlksnext  29856  wwlksnextwrd  29860  clwwlkccatlem  29951  mdslmd1lem1  32287  mdslmd1lem2  32288  dfon2  35765  cgrextend  35981  brsegle  36081  finxpsuclem  37370  poimirlem18  37617  poimirlem21  37620  brabg2  37696  dfatcolem  47240  iccelpart  47418