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

Theorem exbiri 811
Description: Inference form of exbir 41636. This proof is exbiriVD 42012 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 481 . 2 (((𝜑𝜓) ∧ 𝜃) → 𝜒)
32exp31 423 1 (𝜑 → (𝜓 → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  biimp3ar  1471  ralxfrd  5275  ralxfrd2  5279  tfrlem9  8050  mapfset  8460  sbthlem1  8677  addcanpr  10546  axpre-sup  10669  lbreu  11668  zmax  12427  uzsubsubfz  13020  elfzodifsumelfzo  13194  pfxccatin12lem3  14183  cshwidxmod  14254  prmgaplem6  16492  ucnima  23033  gausslemma2dlem1a  26101  usgredg2vlem2  27168  umgr2v2enb1  27468  wwlksnext  27831  wwlksnextwrd  27835  clwwlkccatlem  27926  mdslmd1lem1  30260  mdslmd1lem2  30261  dfon2  33340  cgrextend  33948  brsegle  34048  finxpsuclem  35191  poimirlem18  35418  poimirlem21  35421  brabg2  35497  dfatcolem  44280  iccelpart  44419
  Copyright terms: Public domain W3C validator