Theorem orim12d 966

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

Syntax hints:   → wi 4   ∨ wo 847

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 848

This theorem is referenced by:  orim1d  967  orim2d  968  3orim123d  1446  preq12b  4814  propeqop  5467  fr2nr  5615  sossfld  6159  ordtri3or  6364  ordelinel  6435  funun  6562  soisores  7302  sorpsscmpl  7710  sucexeloniOLD  7786  ordunisuc2  7820  fnse  8112  oaord  8511  omord2  8531  omcan  8533  oeord  8552  oecan  8553  nnaord  8583  nnmord  8596  omsmo  8622  swoer  8702  unxpwdom  9542  rankxplim3  9834  cdainflem  10141  ackbij2  10195  sornom  10230  fin23lem20  10290  fpwwe2lem9  10592  inatsk  10731  ltadd2  11278  ltord1  11704  ltmul1  12032  lt2msq  12068  zle0orge1  12546  mul2lt0bi  13059  xmullem2  13225  difreicc  13445  fzospliti  13652  om2uzlti  13915  om2uzlt2i  13916  om2uzf1oi  13918  absor  15266  ruclem12  16209  dvdslelem  16279  odd2np1lem  16310  odd2np1  16311  isprm6  16684  pythagtrip  16805  pc2dvds  16850  mreexexlem4d  17608  mreexexd  17609  ablsimpgprmd  20047  irredrmul  20336  znidomb  21471  mplsubrglem  21913  ppttop  22894  filconn  23770  trufil  23797  ufildr  23818  plycj  26183  plycjOLD  26185  cosord  26440  logdivlt  26530  isosctrlem2  26729  atans2  26841  wilthlem2  26979  basellem3  26993  lgsdir2lem4  27239  pntpbnd1  27497  nofv  27569  nolesgn2o  27583  noetalem1  27653  om2noseqlt2  28194  om2noseqf1o  28195  mirhl  28606  axcontlem2  28892  axcontlem4  28894  ex-natded5.13-2  30345  hiidge0  31027  chirredlem4  32322  orim12da  32387  disjxpin  32517  nn0xmulclb  32694  iocinif  32704  pmtrcnelor  33048  isprmidlc  33418  rhmpreimaprmidl  33422  minplyirred  33701  erdszelem11  35188  erdsze2lem2  35191  satfv1  35350  satfdmlem  35355  fmla1  35374  satffunlem2lem2  35393  pm3.48ALT  35673  dfon2lem5  35775  btwnconn1lem14  36088  btwnconn2  36090  bj-nnford  36739  poimir  37647  ispridlc  38064  lcvexchlem4  39030  lcvexchlem5  39031  paddss1  39811  paddss2  39812  mulgt0con1dlem  42457  rexzrexnn0  42792  pell14qrdich  42857  acongsym  42965  dvdsacongtr  42973  or3or  44012  clsk1indlem3  44032  mnringmulrcld  44217  nn0eo  48517  prelrrx2b  48703  itscnhlc0xyqsol  48754  itschlc0xyqsol  48756  inlinecirc02plem  48775