Theorem exbiri 811

Description: Inference form of exbir 44906. This proof is exbiriVD 45280 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  5350  ralxfrd2  5354  tfrlem9  8324  mapfset  8797  sbthlem1  9025  addcanpr  10969  axpre-sup  11092  lbreu  12106  zmax  12895  uzsubsubfz  13500  elfzodifsumelfzo  13686  pfxccatin12lem3  14694  cshwidxmod  14765  prmgaplem6  17027  ucnima  24245  gausslemma2dlem1a  27328  usgredg2vlem2  29295  umgr2v2enb1  29595  wwlksnext  29961  wwlksnextwrd  29965  clwwlkccatlem  30059  mdslmd1lem1  32396  mdslmd1lem2  32397  dfon2  35972  cgrextend  36190  brsegle  36290  finxpsuclem  37713  poimirlem18  37959  poimirlem21  37962  brabg2  38038  dfatcolem  47703  iccelpart  47893