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  1445  preq12b  4849  propeqop  5511  fr2nr  5661  sossfld  6205  ordtri3or  6415  ordelinel  6484  funun  6611  soisores  7348  sorpsscmpl  7755  sucexeloniOLD  7831  suceloniOLD  7833  ordunisuc2  7866  fnse  8159  oaord  8586  omord2  8606  omcan  8608  oeord  8627  oecan  8628  nnaord  8658  nnmord  8671  omsmo  8697  swoer  8777  unxpwdom  9630  rankxplim3  9922  cdainflem  10229  ackbij2  10283  sornom  10318  fin23lem20  10378  fpwwe2lem9  10680  inatsk  10819  ltadd2  11366  ltord1  11790  ltmul1  12118  lt2msq  12154  zle0orge1  12632  mul2lt0bi  13142  xmullem2  13308  difreicc  13525  fzospliti  13732  om2uzlti  13992  om2uzlt2i  13993  om2uzf1oi  13995  absor  15340  ruclem12  16278  dvdslelem  16347  odd2np1lem  16378  odd2np1  16379  isprm6  16752  pythagtrip  16873  pc2dvds  16918  mreexexlem4d  17691  mreexexd  17692  ablsimpgprmd  20136  irredrmul  20428  znidomb  21581  mplsubrglem  22025  ppttop  23015  filconn  23892  trufil  23919  ufildr  23940  plycj  26318  plycjOLD  26320  cosord  26574  logdivlt  26664  isosctrlem2  26863  atans2  26975  wilthlem2  27113  basellem3  27127  lgsdir2lem4  27373  pntpbnd1  27631  nofv  27703  nolesgn2o  27717  noetalem1  27787  om2noseqlt2  28307  om2noseqf1o  28308  mirhl  28688  axcontlem2  28981  axcontlem4  28983  ex-natded5.13-2  30436  hiidge0  31118  chirredlem4  32413  orim12da  32478  disjxpin  32602  nn0xmulclb  32776  iocinif  32784  pmtrcnelor  33112  isprmidlc  33476  rhmpreimaprmidl  33480  minplyirred  33755  erdszelem11  35207  erdsze2lem2  35210  satfv1  35369  satfdmlem  35374  fmla1  35393  satffunlem2lem2  35412  pm3.48ALT  35692  dfon2lem5  35789  btwnconn1lem14  36102  btwnconn2  36104  bj-nnford  36753  poimir  37661  ispridlc  38078  lcvexchlem4  39039  lcvexchlem5  39040  paddss1  39820  paddss2  39821  mulgt0con1dlem  42492  rexzrexnn0  42820  pell14qrdich  42885  acongsym  42993  dvdsacongtr  43001  or3or  44041  clsk1indlem3  44061  mnringmulrcld  44252  nn0eo  48454  prelrrx2b  48640  itscnhlc0xyqsol  48691  itschlc0xyqsol  48693  inlinecirc02plem  48712