Theorem orim12d 791

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

Syntax hints:   → wi 4   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  792  orim2d  793  3orim123d  1354  19.33b2  1675  eqifdc  3639  preq12b  3848  prel12  3849  exmidsssnc  4288  funun  5365  nnsucelsuc  6650  nnaord  6668  nnmord  6676  swoer  6721  fidceq  7044  fin0or  7061  fidcen  7074  enomnilem  7321  exmidomni  7325  fodjuomnilemres  7331  ltsopr  7799  cauappcvgprlemloc  7855  caucvgprlemloc  7878  caucvgprprlemloc  7906  suplocexprlemloc  7924  mulextsr1lem  7983  suplocsrlemb  8009  axpre-suploclemres  8104  reapcotr  8761  apcotr  8770  mulext1  8775  mulext  8777  mul0eqap  8833  peano2z  9498  zeo  9568  uzm1  9770  eluzdc  9822  fzospliti  10391  frec2uzltd  10642  absext  11595  qabsor  11607  maxleast  11745  dvdslelemd  12375  odd2np1lem  12404  odd2np1  12405  isprm6  12690  pythagtrip  12827  pc2dvds  12874  ennnfonelemrnh  13008  aprcotr  14270  znidomb  14643  dedekindeulemloc  15314  suplociccreex  15319  dedekindicclemloc  15323  ivthinclemloc  15336  ivthdichlem  15346  plycj  15456  cos11  15548  lgsdir2lem4  15731  uzdcinzz  16271  bj-charfunr  16282  bj-findis  16451  nninfomnilem  16498  isomninnlem  16512