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  1472  preq12b  4813  trun  5227  propeqop  5488  fr2nr  5636  sossfld  6183  ordtri3or  6394  ordelinel  6465  funun  6583  soisores  7332  sorpsscmpl  7739  ordunisuc2  7844  fnse  8135  oaord  8538  omord2  8558  omcan  8560  oeord  8580  oecan  8581  nnaord  8611  nnmord  8624  omsmo  8650  swoer  8732  unxpwdom  9565  rankxplim3  9867  cdainflem  10194  ackbij2  10248  sornom  10283  fin23lem20  10343  fpwwe2lem9  10652  inatsk  10791  ltadd2  11342  ltord1  11768  ltmul1  12093  lt2msq  12128  zle0orge1  12636  mul2lt0bi  13154  xmullem2  13321  difreicc  13541  fzospliti  13751  om2uzlti  14018  om2uzlt2i  14019  om2uzf1oi  14021  absor  15391  ruclem12  16335  dvdslelem  16405  odd2np1lem  16436  odd2np1  16437  isprm6  16811  pythagtrip  16932  pc2dvds  16977  mreexexlem4d  17741  mreexexd  17742  chnccat  18720  ablsimpgprmd  20250  irredrmul  20574  isprmidlc  21541  rhmpreimaprmidl  21548  znidomb  21780  mplsubrglem  22224  ppttop  23238  filconn  24115  trufil  24142  ufildr  24163  plycj  26510  plycjOLD  26512  cosord  26776  logdivlt  26866  isosctrlem2  27064  atans2  27176  wilthlem2  27313  basellem3  27327  lgsdir2lem4  27572  pntpbnd1  27830  nofv  27901  nolesgn2o  27915  noetalem1  27985  om2noseqlt2  28573  om2noseqf1o  28574  zcuts0  28681  mirhl  29038  axcontlem2  29430  axcontlem4  29432  ex-natded5.13-2  30904  hiidge0  31587  chirredlem4  32882  disjxpin  33069  nn0xmulclb  33250  iocinif  33260  pmtrcnelor  33539  minplyirred  34229  erdszelem11  35788  erdsze2lem2  35791  satfv1  35950  satfdmlem  35955  fmla1  35974  satffunlem2lem2  35993  pm3.48ALT  36273  dfon2lem5  36372  btwnconn1lem14  36688  btwnconn2  36690  bj-nnford  37498  poimir  38410  ispridlc  38828  lcvexchlem4  39918  lcvexchlem5  39919  paddss1  40698  paddss2  40699  mulgt0con1dlem  43365  rexzrexnn0  43653  pell14qrdich  43718  acongsym  43825  dvdsacongtr  43833  or3or  44871  clsk1indlem3  44891  mnringmulrcld  45074  grlimprclnbgrvtx  48923  nn0eo  49466  prelrrx2b  49652  itscnhlc0xyqsol  49703  itschlc0xyqsol  49705  inlinecirc02plem  49724