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 38193. This proof is exbiriVD 38599 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  4844  ralxfrd2  4849  tfrlem9  7433  sbthlem1  8021  addcanpr  9819  axpre-sup  9941  lbreu  10924  zmax  11736  uzsubsubfz  12312  elfzodifsumelfzo  12481  swrdccatin12lem3  13434  cshwidxmod  13493  prmgaplem6  15691  ucnima  22004  gausslemma2dlem1a  25003  usgredg2vlem2  26024  umgr2v2enb1  26321  wwlksnextwrd  26674  numclwlk1lem2f1  27095  mdslmd1lem1  29051  mdslmd1lem2  29052  dfon2  31425  cgrextend  31784  brsegle  31884  finxpsuclem  32893  poimirlem18  33086  poimirlem21  33089  brabg2  33169  iccelpart  40688
  Copyright terms: Public domain W3C validator