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  4794  propeqop  5455  fr2nr  5601  sossfld  6144  ordtri3or  6349  ordelinel  6420  funun  6538  soisores  7275  sorpsscmpl  7681  ordunisuc2  7788  fnse  8076  oaord  8475  omord2  8495  omcan  8497  oeord  8517  oecan  8518  nnaord  8548  nnmord  8561  omsmo  8587  swoer  8668  unxpwdom  9497  rankxplim3  9796  cdainflem  10101  ackbij2  10155  sornom  10190  fin23lem20  10250  fpwwe2lem9  10553  inatsk  10692  ltadd2  11241  ltord1  11667  ltmul1  11996  lt2msq  12032  zle0orge1  12532  mul2lt0bi  13041  xmullem2  13208  difreicc  13428  fzospliti  13637  om2uzlti  13903  om2uzlt2i  13904  om2uzf1oi  13906  absor  15253  ruclem12  16199  dvdslelem  16269  odd2np1lem  16300  odd2np1  16301  isprm6  16675  pythagtrip  16796  pc2dvds  16841  mreexexlem4d  17604  mreexexd  17605  chnccat  18583  ablsimpgprmd  20083  irredrmul  20398  znidomb  21551  mplsubrglem  21992  ppttop  22982  filconn  23858  trufil  23885  ufildr  23906  plycj  26252  plycjOLD  26254  cosord  26508  logdivlt  26598  isosctrlem2  26796  atans2  26908  wilthlem2  27046  basellem3  27060  lgsdir2lem4  27305  pntpbnd1  27563  nofv  27635  nolesgn2o  27649  noetalem1  27719  om2noseqlt2  28306  om2noseqf1o  28307  zcuts0  28414  mirhl  28761  axcontlem2  29048  axcontlem4  29050  ex-natded5.13-2  30501  hiidge0  31184  chirredlem4  32479  orim12da  32542  disjxpin  32673  nn0xmulclb  32859  iocinif  32869  pmtrcnelor  33167  isprmidlc  33522  rhmpreimaprmidl  33526  minplyirred  33871  erdszelem11  35399  erdsze2lem2  35402  satfv1  35561  satfdmlem  35566  fmla1  35585  satffunlem2lem2  35604  pm3.48ALT  35884  dfon2lem5  35983  btwnconn1lem14  36298  btwnconn2  36300  bj-nnford  37070  poimir  37988  ispridlc  38405  lcvexchlem4  39497  lcvexchlem5  39498  paddss1  40277  paddss2  40278  mulgt0con1dlem  42928  rexzrexnn0  43250  pell14qrdich  43315  acongsym  43422  dvdsacongtr  43430  or3or  44468  clsk1indlem3  44488  mnringmulrcld  44673  grlimprclnbgrvtx  48487  nn0eo  49016  prelrrx2b  49202  itscnhlc0xyqsol  49253  itschlc0xyqsol  49255  inlinecirc02plem  49274