MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exbiri Structured version   Visualization version   GIF version

Theorem exbiri 845
Description: Inference form of exbir 39515. This proof is exbiriVD 39901 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
StepHypRef Expression
1 exbiri.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21biimpar 471 . 2 (((𝜑𝜓) ∧ 𝜃) → 𝜒)
32exp31 412 1 (𝜑 → (𝜓 → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386
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 199  df-an 387
This theorem is referenced by:  biimp3ar  1598  ralxfrd  5108  ralxfrd2  5112  tfrlem9  7747  sbthlem1  8339  addcanpr  10183  axpre-sup  10306  lbreu  11303  zmax  12068  uzsubsubfz  12656  elfzodifsumelfzo  12829  swrdccatin12lem3  13830  cshwidxmod  13924  prmgaplem6  16131  ucnima  22455  gausslemma2dlem1a  25503  usgredg2vlem2  26522  umgr2v2enb1  26824  wwlksnextwrd  27211  wwlksnextwrdOLD  27216  mdslmd1lem1  29728  mdslmd1lem2  29729  dfon2  32224  cgrextend  32643  brsegle  32743  finxpsuclem  33772  poimirlem18  33964  poimirlem21  33967  brabg2  34046  dfatcolem  42150  iccelpart  42250
  Copyright terms: Public domain W3C validator