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

Theorem orim1d 968
Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
Hypothesis
Ref Expression
orim1d.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
orim1d (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))

Proof of Theorem orim1d
StepHypRef Expression
1 orim1d.1 . 2 (𝜑 → (𝜓𝜒))
2 idd 24 . 2 (𝜑 → (𝜃𝜃))
31, 2orim12d 967 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 848
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 207  df-an 396  df-or 849
This theorem is referenced by:  pm2.38  971  pm2.8  975  pm2.73  976  pm2.74  977  pm2.82  978  moeq3  3718  unss1  4185  ordtri2or2  6483  gchor  10667  relin01  11787  icombl  25599  ioombl  25600  coltr  28655  frgrregorufrg  30345  cycpmco2  33153  fmlasuc  35391  satffunlem1lem2  35408  satffunlem2lem2  35411  naim1  36390  onsucconni  36438  dnibndlem13  36491  mblfinlem2  37665  leat3  39296  meetat2  39298  paddss1  39819  onov0suclim  43287  dflim5  43342  ordsssucim  43415
  Copyright terms: Public domain W3C validator