Theorem orim12d 798

Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)

Hypotheses

Ref	Expression
orim12d.1	⊢ (𝜑 → (𝜓 → 𝜒))
orim12d.2	⊢ (𝜑 → (𝜃 → 𝜏))

Assertion

Ref	Expression
orim12d	⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))

Proof of Theorem orim12d

Step	Hyp	Ref	Expression
1		orim12d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		orim12d.2	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
3		pm3.48 797	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ∨ wo 720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  799  orim2d  800  3orim123d  1361  19.33b2  1682  eqifdc  3677  preq12b  3893  prel12  3894  exmidsssnc  4338  funun  5420  nnsucelsuc  6758  nnaord  6776  nnmord  6784  swoer  6829  fidceq  7165  fin0or  7184  fidcen  7197  enomnilem  7472  exmidomni  7476  fodjuomnilemres  7482  ltsopr  7957  cauappcvgprlemloc  8013  caucvgprlemloc  8036  caucvgprprlemloc  8064  suplocexprlemloc  8082  mulextsr1lem  8141  suplocsrlemb  8167  axpre-suploclemres  8262  reapcotr  8920  apcotr  8929  mulext1  8934  mulext  8936  mul0eqap  8994  peano2z  9663  zeo  9734  uzm1  9936  eluzdc  9993  fzospliti  10568  frec2uzltd  10823  absext  11812  qabsor  11824  maxleast  11962  dvdslelemd  12593  odd2np1lem  12622  odd2np1  12623  isprm6  12908  pythagtrip  13045  pc2dvds  13092  ennnfonelemrnh  13290  aprcotr  14580  znidomb  14976  dedekindeulemloc  15703  suplociccreex  15708  dedekindicclemloc  15712  ivthinclemloc  15725  ivthdichlem  15735  plycj  15845  cos11  15937  lgsdir2lem4  16133  uzdcinzz  16809  bj-charfunr  16819  bj-findis  16988  nninfomnilem  17035  isomninnlem  17053