Theorem orim12d 793

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

Syntax hints:   → wi 4   ∨ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  794  orim2d  795  3orim123d  1356  19.33b2  1677  eqifdc  3642  preq12b  3853  prel12  3854  exmidsssnc  4293  funun  5371  nnsucelsuc  6659  nnaord  6677  nnmord  6685  swoer  6730  fidceq  7056  fin0or  7075  fidcen  7088  enomnilem  7337  exmidomni  7341  fodjuomnilemres  7347  ltsopr  7816  cauappcvgprlemloc  7872  caucvgprlemloc  7895  caucvgprprlemloc  7923  suplocexprlemloc  7941  mulextsr1lem  8000  suplocsrlemb  8026  axpre-suploclemres  8121  reapcotr  8778  apcotr  8787  mulext1  8792  mulext  8794  mul0eqap  8850  peano2z  9515  zeo  9585  uzm1  9787  eluzdc  9844  fzospliti  10413  frec2uzltd  10666  absext  11625  qabsor  11637  maxleast  11775  dvdslelemd  12406  odd2np1lem  12435  odd2np1  12436  isprm6  12721  pythagtrip  12858  pc2dvds  12905  ennnfonelemrnh  13039  aprcotr  14302  znidomb  14675  dedekindeulemloc  15346  suplociccreex  15351  dedekindicclemloc  15355  ivthinclemloc  15368  ivthdichlem  15378  plycj  15488  cos11  15580  lgsdir2lem4  15763  uzdcinzz  16415  bj-charfunr  16426  bj-findis  16595  nninfomnilem  16641  isomninnlem  16655