Theorem orim12d 798

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  orim1d  799  orim2d  800  3orim123d  1361  19.33b2  1682  eqifdc  3677  preq12b  3895  prel12  3896  exmidsssnc  4342  funun  5425  nnsucelsuc  6768  nnaord  6786  nnmord  6794  swoer  6839  fidceq  7176  fin0or  7195  fidcen  7208  enomnilem  7485  exmidomni  7489  fodjuomnilemres  7495  ltsopr  7970  cauappcvgprlemloc  8026  caucvgprlemloc  8049  caucvgprprlemloc  8077  suplocexprlemloc  8095  mulextsr1lem  8154  suplocsrlemb  8180  axpre-suploclemres  8275  reapcotr  8935  apcotr  8944  mulext1  8949  mulext  8951  mul0eqap  9009  peano2z  9692  zeo  9763  uzm1  9970  eluzdc  10027  fzospliti  10603  frec2uzltd  10862  absext  11852  qabsor  11864  maxleast  12003  dvdslelemd  12636  odd2np1lem  12665  odd2np1  12666  isprm6  12952  nn0sqdcq  13014  sqrtrirr  13015  pythagtrip  13092  pc2dvds  13139  ennnfonelemrnh  13366  gsum2d2fi  14275  aprcotr  14707  znidomb  15103  dedekindeulemloc  15857  suplociccreex  15862  dedekindicclemloc  15866  ivthinclemloc  15879  ivthdichlem  15889  plycj  15999  cos11  16093  zprmlogbaplem2  16228  lgsdir2lem4  16367  uzdcinzz  17043  bj-charfunr  17053  bj-findis  17222  nninfomnilem  17279  isomninnlem  17297