Theorem exbiri 811

Description: Inference form of exbir 44924. This proof is exbiriVD 45298 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  5345  ralxfrd2  5349  tfrlem9  8317  mapfset  8790  sbthlem1  9018  addcanpr  10960  axpre-sup  11083  lbreu  12097  zmax  12886  uzsubsubfz  13491  elfzodifsumelfzo  13677  pfxccatin12lem3  14685  cshwidxmod  14756  prmgaplem6  17018  ucnima  24255  gausslemma2dlem1a  27342  usgredg2vlem2  29309  umgr2v2enb1  29610  wwlksnext  29976  wwlksnextwrd  29980  clwwlkccatlem  30074  mdslmd1lem1  32411  mdslmd1lem2  32412  dfon2  35988  cgrextend  36206  brsegle  36306  finxpsuclem  37727  poimirlem18  37973  poimirlem21  37976  brabg2  38052  dfatcolem  47715  iccelpart  47905