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

Theorem exbiri 810
Description: Inference form of exbir 43110. This proof is exbiriVD 43486 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 479 . 2 (((𝜑𝜓) ∧ 𝜃) → 𝜒)
32exp31 421 1 (𝜑 → (𝜓 → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  biimp3ar  1471  ralxfrd  5402  ralxfrd2  5406  tfrlem9  8372  mapfset  8832  sbthlem1  9071  addcanpr  11028  axpre-sup  11151  lbreu  12151  zmax  12916  uzsubsubfz  13510  elfzodifsumelfzo  13685  pfxccatin12lem3  14669  cshwidxmod  14740  prmgaplem6  16976  ucnima  23755  gausslemma2dlem1a  26835  usgredg2vlem2  28450  umgr2v2enb1  28750  wwlksnext  29114  wwlksnextwrd  29118  clwwlkccatlem  29209  mdslmd1lem1  31543  mdslmd1lem2  31544  dfon2  34695  cgrextend  34911  brsegle  35011  finxpsuclem  36183  poimirlem18  36411  poimirlem21  36414  brabg2  36490  dfatcolem  45836  iccelpart  45974
  Copyright terms: Public domain W3C validator