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

Theorem exbiri 651
Description: Inference form of exbir 38205. This proof is exbiriVD 38611 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 502 . 2 (((𝜑𝜓) ∧ 𝜃) → 𝜒)
32exp31 629 1 (𝜑 → (𝜓 → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 386
This theorem is referenced by:  biimp3ar  1430  ralxfrd  4849  ralxfrd2  4854  tfrlem9  7441  sbthlem1  8030  addcanpr  9828  axpre-sup  9950  lbreu  10933  zmax  11745  uzsubsubfz  12321  elfzodifsumelfzo  12490  swrdccatin12lem3  13443  cshwidxmod  13502  prmgaplem6  15703  ucnima  22025  gausslemma2dlem1a  25024  usgredg2vlem2  26045  umgr2v2enb1  26342  wwlksnextwrd  26695  numclwlk1lem2f1  27116  mdslmd1lem1  29072  mdslmd1lem2  29073  dfon2  31451  cgrextend  31810  brsegle  31910  finxpsuclem  32905  poimirlem18  33098  poimirlem21  33101  brabg2  33181  iccelpart  40697
  Copyright terms: Public domain W3C validator