Theorem orim12d 966

Description: Disjoin antecedents and consequents in a deduction. See orim12dALT 911 for a proof which does not depend on df-an 396. (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 965	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  orim1d  967  orim2d  968  3orim123d  1446  preq12b  4817  propeqop  5470  fr2nr  5618  sossfld  6162  ordtri3or  6367  ordelinel  6438  funun  6565  soisores  7305  sorpsscmpl  7713  sucexeloniOLD  7789  ordunisuc2  7823  fnse  8115  oaord  8514  omord2  8534  omcan  8536  oeord  8555  oecan  8556  nnaord  8586  nnmord  8599  omsmo  8625  swoer  8705  unxpwdom  9549  rankxplim3  9841  cdainflem  10148  ackbij2  10202  sornom  10237  fin23lem20  10297  fpwwe2lem9  10599  inatsk  10738  ltadd2  11285  ltord1  11711  ltmul1  12039  lt2msq  12075  zle0orge1  12553  mul2lt0bi  13066  xmullem2  13232  difreicc  13452  fzospliti  13659  om2uzlti  13922  om2uzlt2i  13923  om2uzf1oi  13925  absor  15273  ruclem12  16216  dvdslelem  16286  odd2np1lem  16317  odd2np1  16318  isprm6  16691  pythagtrip  16812  pc2dvds  16857  mreexexlem4d  17615  mreexexd  17616  ablsimpgprmd  20054  irredrmul  20343  znidomb  21478  mplsubrglem  21920  ppttop  22901  filconn  23777  trufil  23804  ufildr  23825  plycj  26190  plycjOLD  26192  cosord  26447  logdivlt  26537  isosctrlem2  26736  atans2  26848  wilthlem2  26986  basellem3  27000  lgsdir2lem4  27246  pntpbnd1  27504  nofv  27576  nolesgn2o  27590  noetalem1  27660  om2noseqlt2  28201  om2noseqf1o  28202  mirhl  28613  axcontlem2  28899  axcontlem4  28901  ex-natded5.13-2  30352  hiidge0  31034  chirredlem4  32329  orim12da  32394  disjxpin  32524  nn0xmulclb  32701  iocinif  32711  pmtrcnelor  33055  isprmidlc  33425  rhmpreimaprmidl  33429  minplyirred  33708  erdszelem11  35195  erdsze2lem2  35198  satfv1  35357  satfdmlem  35362  fmla1  35381  satffunlem2lem2  35400  pm3.48ALT  35680  dfon2lem5  35782  btwnconn1lem14  36095  btwnconn2  36097  bj-nnford  36746  poimir  37654  ispridlc  38071  lcvexchlem4  39037  lcvexchlem5  39038  paddss1  39818  paddss2  39819  mulgt0con1dlem  42464  rexzrexnn0  42799  pell14qrdich  42864  acongsym  42972  dvdsacongtr  42980  or3or  44019  clsk1indlem3  44039  mnringmulrcld  44224  nn0eo  48521  prelrrx2b  48707  itscnhlc0xyqsol  48758  itschlc0xyqsol  48760  inlinecirc02plem  48779