Theorem exbiri 811

Description: Inference form of exbir 44499. This proof is exbiriVD 44874 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  1472  ralxfrd  5408  ralxfrd2  5412  tfrlem9  8425  mapfset  8890  sbthlem1  9123  addcanpr  11086  axpre-sup  11209  lbreu  12218  zmax  12987  uzsubsubfz  13586  elfzodifsumelfzo  13770  pfxccatin12lem3  14770  cshwidxmod  14841  prmgaplem6  17094  ucnima  24290  gausslemma2dlem1a  27409  usgredg2vlem2  29243  umgr2v2enb1  29544  wwlksnext  29913  wwlksnextwrd  29917  clwwlkccatlem  30008  mdslmd1lem1  32344  mdslmd1lem2  32345  dfon2  35793  cgrextend  36009  brsegle  36109  finxpsuclem  37398  poimirlem18  37645  poimirlem21  37648  brabg2  37724  dfatcolem  47267  iccelpart  47420