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

Theorem exbiri 653
 Description: Inference form of exbir 39155. This proof is exbiriVD 39557 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 503 . 2 (((𝜑𝜓) ∧ 𝜃) → 𝜒)
32exp31 631 1 (𝜑 → (𝜓 → (𝜃𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383 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 197  df-an 385 This theorem is referenced by:  biimp3ar  1570  ralxfrd  5016  ralxfrd2  5021  tfrlem9  7638  sbthlem1  8223  addcanpr  10031  axpre-sup  10153  lbreu  11136  zmax  11949  uzsubsubfz  12527  elfzodifsumelfzo  12699  swrdccatin12lem3  13661  cshwidxmod  13720  prmgaplem6  15933  ucnima  22257  gausslemma2dlem1a  25260  usgredg2vlem2  26288  umgr2v2enb1  26603  wwlksnextwrd  26986  mdslmd1lem1  29464  mdslmd1lem2  29465  dfon2  31973  cgrextend  32392  brsegle  32492  finxpsuclem  33516  poimirlem18  33709  poimirlem21  33712  brabg2  33792  iccelpart  41848
 Copyright terms: Public domain W3C validator