Theorem orim12d 786

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

Syntax hints:   → wi 4   ∨ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  787  orim2d  788  3orim123d  1320  19.33b2  1629  eqifdc  3570  preq12b  3771  prel12  3772  exmidsssnc  4204  funun  5261  nnsucelsuc  6492  nnaord  6510  nnmord  6518  swoer  6563  fidceq  6869  fin0or  6886  enomnilem  7136  exmidomni  7140  fodjuomnilemres  7146  ltsopr  7595  cauappcvgprlemloc  7651  caucvgprlemloc  7674  caucvgprprlemloc  7702  suplocexprlemloc  7720  mulextsr1lem  7779  suplocsrlemb  7805  axpre-suploclemres  7900  reapcotr  8555  apcotr  8564  mulext1  8569  mulext  8571  mul0eqap  8627  peano2z  9289  zeo  9358  uzm1  9558  eluzdc  9610  fzospliti  10176  frec2uzltd  10403  absext  11072  qabsor  11084  maxleast  11222  dvdslelemd  11849  odd2np1lem  11877  odd2np1  11878  isprm6  12147  pythagtrip  12283  pc2dvds  12329  ennnfonelemrnh  12417  aprcotr  13375  dedekindeulemloc  14100  suplociccreex  14105  dedekindicclemloc  14109  ivthinclemloc  14122  cos11  14277  lgsdir2lem4  14435  uzdcinzz  14553  bj-charfunr  14565  bj-findis  14734  nninfomnilem  14770  isomninnlem  14781