Theorem orim12d 790

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

Syntax hints:   → wi 4   ∨ wo 712

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 713

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  791  orim2d  792  3orim123d  1335  19.33b2  1655  eqifdc  3619  preq12b  3827  prel12  3828  exmidsssnc  4266  funun  5338  nnsucelsuc  6607  nnaord  6625  nnmord  6633  swoer  6678  fidceq  6999  fin0or  7016  enomnilem  7273  exmidomni  7277  fodjuomnilemres  7283  ltsopr  7751  cauappcvgprlemloc  7807  caucvgprlemloc  7830  caucvgprprlemloc  7858  suplocexprlemloc  7876  mulextsr1lem  7935  suplocsrlemb  7961  axpre-suploclemres  8056  reapcotr  8713  apcotr  8722  mulext1  8727  mulext  8729  mul0eqap  8785  peano2z  9450  zeo  9520  uzm1  9721  eluzdc  9773  fzospliti  10342  frec2uzltd  10592  absext  11540  qabsor  11552  maxleast  11690  dvdslelemd  12320  odd2np1lem  12349  odd2np1  12350  isprm6  12635  pythagtrip  12772  pc2dvds  12819  ennnfonelemrnh  12953  aprcotr  14214  znidomb  14587  dedekindeulemloc  15258  suplociccreex  15263  dedekindicclemloc  15267  ivthinclemloc  15280  ivthdichlem  15290  plycj  15400  cos11  15492  lgsdir2lem4  15675  uzdcinzz  16072  bj-charfunr  16083  bj-findis  16252  nninfomnilem  16295  isomninnlem  16309