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 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))

This proof depends on syntax axioms:   → wi 4   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  orim1d  799  orim2d  800  3orim123d  1361  19.33b2  1682  eqifdc  3677  preq12b  3895  prel12  3896  exmidsssnc  4340  funun  5422  nnsucelsuc  6764  nnaord  6782  nnmord  6790  swoer  6835  fidceq  7171  fin0or  7190  fidcen  7203  enomnilem  7478  exmidomni  7482  fodjuomnilemres  7488  ltsopr  7963  cauappcvgprlemloc  8019  caucvgprlemloc  8042  caucvgprprlemloc  8070  suplocexprlemloc  8088  mulextsr1lem  8147  suplocsrlemb  8173  axpre-suploclemres  8268  reapcotr  8927  apcotr  8936  mulext1  8941  mulext  8943  mul0eqap  9001  peano2z  9682  zeo  9753  uzm1  9955  eluzdc  10012  fzospliti  10587  frec2uzltd  10842  absext  11831  qabsor  11843  maxleast  11981  dvdslelemd  12612  odd2np1lem  12641  odd2np1  12642  isprm6  12927  pythagtrip  13064  pc2dvds  13111  ennnfonelemrnh  13309  aprcotr  14599  znidomb  14995  dedekindeulemloc  15722  suplociccreex  15727  dedekindicclemloc  15731  ivthinclemloc  15744  ivthdichlem  15754  plycj  15864  cos11  15957  lgsdir2lem4  16162  uzdcinzz  16838  bj-charfunr  16848  bj-findis  17017  nninfomnilem  17073  isomninnlem  17091