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  4340  funun  5422  nnsucelsuc  6764  nnaord  6782  nnmord  6790  swoer  6835  fidceq  7171  fin0or  7190  fidcen  7203  enomnilem  7479  exmidomni  7483  fodjuomnilemres  7489  ltsopr  7964  cauappcvgprlemloc  8020  caucvgprlemloc  8043  caucvgprprlemloc  8071  suplocexprlemloc  8089  mulextsr1lem  8148  suplocsrlemb  8174  axpre-suploclemres  8269  reapcotr  8929  apcotr  8938  mulext1  8943  mulext  8945  mul0eqap  9003  peano2z  9685  zeo  9756  uzm1  9963  eluzdc  10020  fzospliti  10596  frec2uzltd  10854  absext  11844  qabsor  11856  maxleast  11995  dvdslelemd  12628  odd2np1lem  12657  odd2np1  12658  isprm6  12944  nn0sqdcq  13006  sqrtrirr  13007  pythagtrip  13084  pc2dvds  13131  ennnfonelemrnh  13358  aprcotr  14648  znidomb  15044  dedekindeulemloc  15772  suplociccreex  15777  dedekindicclemloc  15781  ivthinclemloc  15794  ivthdichlem  15804  plycj  15914  cos11  16007  zprmlogbaplem2  16138  lgsdir2lem4  16272  uzdcinzz  16948  bj-charfunr  16958  bj-findis  17127  nninfomnilem  17183  isomninnlem  17201