Theorem orim12d 879

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

Syntax hints:   → wi 4   ∨ wo 382

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385

This theorem is referenced by:  orim1d  880  orim2d  881  3orim123d  1399  preq12b  4322  prel12  4323  propeqop  4895  fr2nr  5016  sossfld  5499  ordtri3or  5672  ordelinel  5742  funun  5846  soisores  6477  sorpsscmpl  6846  suceloni  6905  ordunisuc2  6936  fnse  7181  oaord  7514  omord2  7534  omcan  7536  oeord  7555  oecan  7556  nnaord  7586  nnmord  7599  omsmo  7621  swoer  7659  unxpwdom  8377  rankxplim3  8627  cdainflem  8896  ackbij2  8948  sornom  8982  fin23lem20  9042  fpwwe2lem10  9340  inatsk  9479  ltadd2  10020  ltord1  10433  ltmul1  10752  lt2msq  10787  mul2lt0bi  11812  xmullem2  11967  difreicc  12175  fzospliti  12369  om2uzlti  12611  om2uzlt2i  12612  om2uzf1oi  12614  absor  13888  ruclem12  14809  dvdslelem  14869  odd2np1lem  14902  odd2np1  14903  isprm6  15264  pythagtrip  15377  pc2dvds  15421  mreexexlem4d  16130  mreexexd  16131  mreexexdOLD  16132  irredrmul  18530  mplsubrglem  19260  znidomb  19729  ppttop  20621  filcon  21497  trufil  21524  ufildr  21545  plycj  23837  cosord  24082  logdivlt  24171  isosctrlem2  24349  atans2  24458  wilthlem2  24595  basellem3  24609  lgsdir2lem4  24853  pntpbnd1  25075  mirhl  25374  axcontlem2  25645  axcontlem4  25647  ex-natded5.13-2  26665  hiidge0  27339  chirredlem4  28636  disjxpin  28783  iocinif  28933  erdszelem11  30437  erdsze2lem2  30440  dfon2lem5  30936  trpredrec  30982  nofv  31054  btwnconn1lem14  31377  btwnconn2  31379  poimir  32612  ispridlc  33039  lcvexchlem4  33342  lcvexchlem5  33343  paddss1  34121  paddss2  34122  rexzrexnn0  36386  pell14qrdich  36451  acongsym  36561  dvdsacongtr  36569  or3or  37339  clsk1indlem3  37361  nn0eo  42116