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

Theorem exbiri 846
Description: Inference form of exbir 39464. This proof is exbiriVD 39850 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 470 . 2 (((𝜑𝜓) ∧ 𝜃) → 𝜒)
32exp31 411 1 (𝜑 → (𝜓 → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385
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 386
This theorem is referenced by:  biimp3ar  1595  ralxfrd  5078  ralxfrd2  5082  tfrlem9  7720  sbthlem1  8312  addcanpr  10156  axpre-sup  10278  lbreu  11265  zmax  12030  uzsubsubfz  12617  elfzodifsumelfzo  12789  swrdccatin12lem3  13794  cshwidxmod  13888  prmgaplem6  16093  ucnima  22413  gausslemma2dlem1a  25442  usgredg2vlem2  26459  umgr2v2enb1  26776  wwlksnextwrd  27169  wwlksnextwrdOLD  27174  mdslmd1lem1  29709  mdslmd1lem2  29710  dfon2  32209  cgrextend  32628  brsegle  32728  finxpsuclem  33732  poimirlem18  33916  poimirlem21  33919  brabg2  33998  dfatcolem  42109  iccelpart  42209
  Copyright terms: Public domain W3C validator