Theorem exbiri 809

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  biimp3ar  1466  ralxfrd  5309  ralxfrd2  5313  tfrlem9  8021  sbthlem1  8627  addcanpr  10468  axpre-sup  10591  lbreu  11591  zmax  12346  uzsubsubfz  12930  elfzodifsumelfzo  13104  pfxccatin12lem3  14094  cshwidxmod  14165  prmgaplem6  16392  ucnima  22890  gausslemma2dlem1a  25941  usgredg2vlem2  27008  umgr2v2enb1  27308  wwlksnext  27671  wwlksnextwrd  27675  clwwlkccatlem  27767  mdslmd1lem1  30102  mdslmd1lem2  30103  dfon2  33037  cgrextend  33469  brsegle  33569  finxpsuclem  34681  poimirlem18  34925  poimirlem21  34928  brabg2  35006  dfatcolem  43474  iccelpart  43613