Theorem orim12d 736

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

Syntax hints:   → wi 4   ∨ wo 665

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim1d  737  orim2d  738  3orim123d  1257  19.33b2  1566  eqifdc  3429  preq12b  3620  prel12  3621  funun  5071  nnsucelsuc  6266  nnaord  6282  nnmord  6290  swoer  6334  fidceq  6639  fin0or  6656  enomnilem  6855  exmidomni  6859  fodjuomnilemres  6864  ltsopr  7216  cauappcvgprlemloc  7272  caucvgprlemloc  7295  caucvgprprlemloc  7323  mulextsr1lem  7386  reapcotr  8136  apcotr  8145  mulext1  8150  mulext  8152  peano2z  8847  zeo  8912  uzm1  9110  eluzdc  9158  fzospliti  9648  frec2uzltd  9871  absext  10557  qabsor  10569  maxleast  10707  dvdslelemd  11183  odd2np1lem  11211  odd2np1  11212  isprm6  11465  uzdcinzz  11971  bj-findis  12147  nninfomnilem  12182