Theorem exbiri 807

Description: Inference form of exbir 41987. This proof is exbiriVD 42363 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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  biimp3ar  1468  ralxfrd  5326  ralxfrd2  5330  tfrlem9  8187  mapfset  8596  sbthlem1  8823  addcanpr  10733  axpre-sup  10856  lbreu  11855  zmax  12614  uzsubsubfz  13207  elfzodifsumelfzo  13381  pfxccatin12lem3  14373  cshwidxmod  14444  prmgaplem6  16685  ucnima  23341  gausslemma2dlem1a  26418  usgredg2vlem2  27496  umgr2v2enb1  27796  wwlksnext  28159  wwlksnextwrd  28163  clwwlkccatlem  28254  mdslmd1lem1  30588  mdslmd1lem2  30589  dfon2  33674  cgrextend  34237  brsegle  34337  finxpsuclem  35495  poimirlem18  35722  poimirlem21  35725  brabg2  35801  dfatcolem  44634  iccelpart  44773