Theorem exbiri 810

Description: Inference form of exbir 44504. This proof is exbiriVD 44878 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  5378  ralxfrd2  5382  tfrlem9  8399  mapfset  8864  sbthlem1  9097  addcanpr  11060  axpre-sup  11183  lbreu  12192  zmax  12961  uzsubsubfz  13563  elfzodifsumelfzo  13747  pfxccatin12lem3  14750  cshwidxmod  14821  prmgaplem6  17076  ucnima  24219  gausslemma2dlem1a  27328  usgredg2vlem2  29205  umgr2v2enb1  29506  wwlksnext  29875  wwlksnextwrd  29879  clwwlkccatlem  29970  mdslmd1lem1  32306  mdslmd1lem2  32307  dfon2  35810  cgrextend  36026  brsegle  36126  finxpsuclem  37415  poimirlem18  37662  poimirlem21  37665  brabg2  37741  dfatcolem  47284  iccelpart  47447