Theorem orim12d 977

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

Syntax hints:   → wi 4   ∨ wo 858

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 209  df-an 400  df-or 859

This theorem is referenced by:  orim1d  978  orim2d  979  3orim123d  1464  preq12b  4807  trun  5217  propeqop  5475  fr2nr  5622  sossfld  6168  ordtri3or  6374  ordelinel  6445  funun  6563  soisores  7307  sorpsscmpl  7713  ordunisuc2  7820  fnse  8108  oaord  8511  omord2  8531  omcan  8533  oeord  8553  oecan  8554  nnaord  8584  nnmord  8597  omsmo  8623  swoer  8705  unxpwdom  9534  rankxplim3  9836  cdainflem  10141  ackbij2  10195  sornom  10231  fin23lem20  10291  fpwwe2lem9  10594  inatsk  10733  ltadd2  11284  ltord1  11710  ltmul1  12038  lt2msq  12074  zle0orge1  12582  mul2lt0bi  13098  xmullem2  13265  difreicc  13485  fzospliti  13694  om2uzlti  13960  om2uzlt2i  13961  om2uzf1oi  13963  absor  15310  ruclem12  16256  dvdslelem  16326  odd2np1lem  16357  odd2np1  16358  isprm6  16732  pythagtrip  16853  pc2dvds  16898  mreexexlem4d  17662  mreexexd  17663  chnccat  18641  ablsimpgprmd  20140  irredrmul  20455  znidomb  21593  mplsubrglem  22035  ppttop  23047  filconn  23923  trufil  23950  ufildr  23971  plycj  26317  plycjOLD  26319  cosord  26573  logdivlt  26663  isosctrlem2  26861  atans2  26973  wilthlem2  27110  basellem3  27124  lgsdir2lem4  27369  pntpbnd1  27627  nofv  27698  nolesgn2o  27712  noetalem1  27782  om2noseqlt2  28370  om2noseqf1o  28371  zcuts0  28478  mirhl  28825  axcontlem2  29112  axcontlem4  29114  ex-natded5.13-2  30564  hiidge0  31247  chirredlem4  32542  orim12da  32605  disjxpin  32737  nn0xmulclb  32923  iocinif  32933  pmtrcnelor  33232  isprmidlc  33594  rhmpreimaprmidl  33599  minplyirred  33969  erdszelem11  35515  erdsze2lem2  35518  satfv1  35677  satfdmlem  35682  fmla1  35701  satffunlem2lem2  35720  pm3.48ALT  36000  dfon2lem5  36099  btwnconn1lem14  36414  btwnconn2  36416  bj-nnford  37196  poimir  38116  ispridlc  38533  lcvexchlem4  39625  lcvexchlem5  39626  paddss1  40405  paddss2  40406  mulgt0con1dlem  43055  rexzrexnn0  43345  pell14qrdich  43410  acongsym  43517  dvdsacongtr  43525  or3or  44563  clsk1indlem3  44583  mnringmulrcld  44768  grlimprclnbgrvtx  48585  nn0eo  49114  prelrrx2b  49300  itscnhlc0xyqsol  49351  itschlc0xyqsol  49353  inlinecirc02plem  49372