Theorem orim12d 979

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  orim12da  980  orim1d  981  orim2d  982  3orim123d  1473  preq12b  4808  trun  5226  propeqop  5483  fr2nr  5632  sossfld  6190  ordtri3or  6413  ordelinel  6484  funun  6606  soisores  7358  sorpsscmpl  7774  ordunisuc2  7879  fnse  8177  oaord  8583  omord2  8603  omcan  8605  oeord  8625  oecan  8626  nnaord  8656  nnmord  8669  omsmo  8695  swoer  8777  unxpwdom  9610  rankxplim3  9925  cdainflem  10293  ackbij2  10347  sornom  10382  fin23lem20  10442  fpwwe2lem9  10751  inatsk  10890  ltadd2  11441  ltord1  11869  ltmul1  12194  lt2msq  12229  zle0orge1  12737  mul2lt0bi  13255  xmullem2  13422  difreicc  13642  fzospliti  13853  om2uzlti  14120  om2uzlt2i  14121  om2uzf1oi  14123  absor  15496  ruclem12  16438  dvdslelem  16508  odd2np1lem  16539  odd2np1  16540  isprm6  16919  pythagtrip  17041  pc2dvds  17086  mreexexlem4d  17850  mreexexd  17851  chnccat  18829  ablsimpgprmd  20361  irredrmul  20687  isprmidlc  21658  rhmpreimaprmidl  21665  znidomb  21897  mplsubrglem  22341  ppttop  23355  filconn  24232  trufil  24259  ufildr  24280  plycj  26626  cosord  26889  logdivlt  26979  isosctrlem2  27177  atans2  27289  wilthlem2  27426  basellem3  27440  lgsdir2lem4  27685  pntpbnd1  27943  nofv  28044  nolesgn2o  28058  noetalem1  28128  om2noseqlt2  28716  om2noseqf1o  28717  zcuts0  28824  mirhl  29181  axcontlem2  29573  axcontlem4  29575  ex-natded5.13-2  31047  hiidge0  31730  chirredlem4  33025  disjxpin  33254  nn0xmulclb  33433  iocinif  33443  pmtrcnelor  33722  minplyirred  34413  dfac16  35846  erdszelem11  36133  erdsze2lem2  36136  satfv1  36295  satfdmlem  36300  fmla1  36319  satffunlem2lem2  36338  pm3.48ALT  36618  dfon2lem5  36727  btwnconn1lem14  37043  btwnconn2  37045  bj-nnford  37837  poimir  38763  ispridlc  39196  lcvexchlem4  40286  lcvexchlem5  40287  paddss1  41066  paddss2  41067  mulgt0con1dlem  43726  rexzrexnn0  44004  pell14qrdich  44069  acongsym  44176  dvdsacongtr  44184  or3or  45215  clsk1indlem3  45235  mnringmulrcld  45418  grlimprclnbgrvtx  49302  nn0eo  49845  itscnhlc0xyqsol  50082  itschlc0xyqsol  50084