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

Theorem exbiri 809
 Description: Inference form of exbir 40810. This proof is exbiriVD 41186 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 480 . 2 (((𝜑𝜓) ∧ 𝜃) → 𝜒)
32exp31 422 1 (𝜑 → (𝜓 → (𝜃𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398 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 209  df-an 399 This theorem is referenced by:  biimp3ar  1466  ralxfrd  5308  ralxfrd2  5312  tfrlem9  8020  sbthlem1  8626  addcanpr  10467  axpre-sup  10590  lbreu  11590  zmax  12344  uzsubsubfz  12928  elfzodifsumelfzo  13102  pfxccatin12lem3  14093  cshwidxmod  14164  prmgaplem6  16391  ucnima  22889  gausslemma2dlem1a  25940  usgredg2vlem2  27007  umgr2v2enb1  27307  wwlksnext  27670  wwlksnextwrd  27674  clwwlkccatlem  27766  mdslmd1lem1  30101  mdslmd1lem2  30102  dfon2  33037  cgrextend  33469  brsegle  33569  finxpsuclem  34677  poimirlem18  34909  poimirlem21  34912  brabg2  34990  dfatcolem  43453  iccelpart  43592
 Copyright terms: Public domain W3C validator