Theorem orim12d 967

Description: Disjoin antecedents and consequents in a deduction. See orim12dALT 912 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 966	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  orim1d  968  orim2d  969  3orim123d  1447  preq12b  4808  propeqop  5463  fr2nr  5609  sossfld  6152  ordtri3or  6357  ordelinel  6428  funun  6546  soisores  7283  sorpsscmpl  7689  ordunisuc2  7796  fnse  8085  oaord  8484  omord2  8504  omcan  8506  oeord  8526  oecan  8527  nnaord  8557  nnmord  8570  omsmo  8596  swoer  8677  unxpwdom  9506  rankxplim3  9805  cdainflem  10110  ackbij2  10164  sornom  10199  fin23lem20  10259  fpwwe2lem9  10562  inatsk  10701  ltadd2  11249  ltord1  11675  ltmul1  12003  lt2msq  12039  zle0orge1  12517  mul2lt0bi  13025  xmullem2  13192  difreicc  13412  fzospliti  13619  om2uzlti  13885  om2uzlt2i  13886  om2uzf1oi  13888  absor  15235  ruclem12  16178  dvdslelem  16248  odd2np1lem  16279  odd2np1  16280  isprm6  16653  pythagtrip  16774  pc2dvds  16819  mreexexlem4d  17582  mreexexd  17583  chnccat  18561  ablsimpgprmd  20058  irredrmul  20375  znidomb  21528  mplsubrglem  21971  ppttop  22963  filconn  23839  trufil  23866  ufildr  23887  plycj  26251  plycjOLD  26253  cosord  26508  logdivlt  26598  isosctrlem2  26797  atans2  26909  wilthlem2  27047  basellem3  27061  lgsdir2lem4  27307  pntpbnd1  27565  nofv  27637  nolesgn2o  27651  noetalem1  27721  om2noseqlt2  28308  om2noseqf1o  28309  zcuts0  28416  mirhl  28763  axcontlem2  29050  axcontlem4  29052  ex-natded5.13-2  30503  hiidge0  31185  chirredlem4  32480  orim12da  32543  disjxpin  32674  nn0xmulclb  32861  iocinif  32871  pmtrcnelor  33184  isprmidlc  33539  rhmpreimaprmidl  33543  minplyirred  33888  erdszelem11  35414  erdsze2lem2  35417  satfv1  35576  satfdmlem  35581  fmla1  35600  satffunlem2lem2  35619  pm3.48ALT  35899  dfon2lem5  35998  btwnconn1lem14  36313  btwnconn2  36315  bj-nnford  36992  poimir  37898  ispridlc  38315  lcvexchlem4  39407  lcvexchlem5  39408  paddss1  40187  paddss2  40188  mulgt0con1dlem  42833  rexzrexnn0  43155  pell14qrdich  43220  acongsym  43327  dvdsacongtr  43335  or3or  44373  clsk1indlem3  44393  mnringmulrcld  44578  grlimprclnbgrvtx  48353  nn0eo  48882  prelrrx2b  49068  itscnhlc0xyqsol  49119  itschlc0xyqsol  49121  inlinecirc02plem  49140