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

Theorem orim1d 967
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 966 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 847
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 848
This theorem is referenced by:  pm2.38  970  pm2.8  974  pm2.73  975  pm2.74  976  pm2.82  977  moeq3  3720  unss1  4194  ordtri2or2  6484  gchor  10664  relin01  11784  icombl  25612  ioombl  25613  coltr  28669  frgrregorufrg  30354  cycpmco2  33135  fmlasuc  35370  satffunlem1lem2  35387  satffunlem2lem2  35390  naim1  36371  onsucconni  36419  dnibndlem13  36472  mblfinlem2  37644  leat3  39276  meetat2  39278  paddss1  39799  onov0suclim  43263  dflim5  43318  ordsssucim  43391
  Copyright terms: Public domain W3C validator