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

Theorem exbiri 650
 Description: Inference form of exbir 37705. This proof is exbiriVD 38111 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 501 . 2 (((𝜑𝜓) ∧ 𝜃) → 𝜒)
32exp31 628 1 (𝜑 → (𝜓 → (𝜃𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ 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 196  df-an 385 This theorem is referenced by:  biimp3ar  1425  ralxfrd  4805  ralxfrd2  4810  tfrlem9  7368  sbthlem1  7955  addcanpr  9747  axpre-sup  9869  lbreu  10852  zmax  11661  uzsubsubfz  12234  elfzodifsumelfzo  12401  swrdccatin12lem3  13341  cshwidxmod  13400  prmgaplem6  15598  ucnima  21895  gausslemma2dlem1a  24890  usgraidx2vlem2  25921  wwlkextwrd  26256  numclwlk1lem2f1  26621  mdslmd1lem1  28568  mdslmd1lem2  28569  dfon2  30941  cgrextend  31285  brsegle  31385  finxpsuclem  32410  poimirlem18  32597  poimirlem21  32600  brabg2  32680  iccelpart  39971  usgredg2vlem2  40453  umgr2v2enb1  40742  wwlksnextwrd  41103  av-numclwlk1lem2f1  41524
 Copyright terms: Public domain W3C validator