Theorem orim12d 788

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

Syntax hints:   → wi 4   ∨ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  789  orim2d  790  3orim123d  1333  19.33b2  1653  eqifdc  3608  preq12b  3813  prel12  3814  exmidsssnc  4251  funun  5320  nnsucelsuc  6584  nnaord  6602  nnmord  6610  swoer  6655  fidceq  6973  fin0or  6990  enomnilem  7247  exmidomni  7251  fodjuomnilemres  7257  ltsopr  7716  cauappcvgprlemloc  7772  caucvgprlemloc  7795  caucvgprprlemloc  7823  suplocexprlemloc  7841  mulextsr1lem  7900  suplocsrlemb  7926  axpre-suploclemres  8021  reapcotr  8678  apcotr  8687  mulext1  8692  mulext  8694  mul0eqap  8750  peano2z  9415  zeo  9485  uzm1  9686  eluzdc  9738  fzospliti  10307  frec2uzltd  10555  absext  11418  qabsor  11430  maxleast  11568  dvdslelemd  12198  odd2np1lem  12227  odd2np1  12228  isprm6  12513  pythagtrip  12650  pc2dvds  12697  ennnfonelemrnh  12831  aprcotr  14091  znidomb  14464  dedekindeulemloc  15135  suplociccreex  15140  dedekindicclemloc  15144  ivthinclemloc  15157  ivthdichlem  15167  plycj  15277  cos11  15369  lgsdir2lem4  15552  uzdcinzz  15808  bj-charfunr  15820  bj-findis  15989  nninfomnilem  16029  isomninnlem  16043