Theorem exbiri 810

Description: Inference form of exbir 43110. This proof is exbiriVD 43486 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 479	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜒)
3	2	exp31 421	1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  biimp3ar  1471  ralxfrd  5402  ralxfrd2  5406  tfrlem9  8372  mapfset  8832  sbthlem1  9071  addcanpr  11028  axpre-sup  11151  lbreu  12151  zmax  12916  uzsubsubfz  13510  elfzodifsumelfzo  13685  pfxccatin12lem3  14669  cshwidxmod  14740  prmgaplem6  16976  ucnima  23755  gausslemma2dlem1a  26835  usgredg2vlem2  28450  umgr2v2enb1  28750  wwlksnext  29114  wwlksnextwrd  29118  clwwlkccatlem  29209  mdslmd1lem1  31543  mdslmd1lem2  31544  dfon2  34695  cgrextend  34911  brsegle  35011  finxpsuclem  36183  poimirlem18  36411  poimirlem21  36414  brabg2  36490  dfatcolem  45836  iccelpart  45974