Theorem orim12d 794

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 793	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ∨ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  795  orim2d  796  3orim123d  1357  19.33b2  1678  eqifdc  3646  preq12b  3858  prel12  3859  exmidsssnc  4299  funun  5378  nnsucelsuc  6702  nnaord  6720  nnmord  6728  swoer  6773  fidceq  7099  fin0or  7118  fidcen  7131  enomnilem  7380  exmidomni  7384  fodjuomnilemres  7390  ltsopr  7859  cauappcvgprlemloc  7915  caucvgprlemloc  7938  caucvgprprlemloc  7966  suplocexprlemloc  7984  mulextsr1lem  8043  suplocsrlemb  8069  axpre-suploclemres  8164  reapcotr  8821  apcotr  8830  mulext1  8835  mulext  8837  mul0eqap  8893  peano2z  9558  zeo  9628  uzm1  9830  eluzdc  9887  fzospliti  10456  frec2uzltd  10709  absext  11684  qabsor  11696  maxleast  11834  dvdslelemd  12465  odd2np1lem  12494  odd2np1  12495  isprm6  12780  pythagtrip  12917  pc2dvds  12964  ennnfonelemrnh  13098  aprcotr  14361  znidomb  14734  dedekindeulemloc  15410  suplociccreex  15415  dedekindicclemloc  15419  ivthinclemloc  15432  ivthdichlem  15442  plycj  15552  cos11  15644  lgsdir2lem4  15830  uzdcinzz  16496  bj-charfunr  16506  bj-findis  16675  nninfomnilem  16724  isomninnlem  16742