Theorem exbiri 811

Description: Inference form of exbir 44829. This proof is exbiriVD 45203 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  1473  ralxfrd  5355  ralxfrd2  5359  tfrlem9  8326  mapfset  8799  sbthlem1  9027  addcanpr  10969  axpre-sup  11092  lbreu  12104  zmax  12870  uzsubsubfz  13474  elfzodifsumelfzo  13659  pfxccatin12lem3  14667  cshwidxmod  14738  prmgaplem6  16996  ucnima  24236  gausslemma2dlem1a  27344  usgredg2vlem2  29311  umgr2v2enb1  29612  wwlksnext  29978  wwlksnextwrd  29982  clwwlkccatlem  30076  mdslmd1lem1  32412  mdslmd1lem2  32413  dfon2  36003  cgrextend  36221  brsegle  36321  finxpsuclem  37646  poimirlem18  37883  poimirlem21  37886  brabg2  37962  dfatcolem  47609  iccelpart  47787