Theorem orim12d 961

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

Syntax hints:   → wi 4   ∨ wo 843

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 206  df-an 395  df-or 844

This theorem is referenced by:  orim1d  962  orim2d  963  3orim123d  1442  preq12b  4850  propeqop  5506  fr2nr  5653  sossfld  6184  ordtri3or  6395  ordelinel  6464  funun  6593  soisores  7326  sorpsscmpl  7726  sucexeloniOLD  7800  suceloniOLD  7802  ordunisuc2  7835  fnse  8121  oaord  8549  omord2  8569  omcan  8571  oeord  8590  oecan  8591  nnaord  8621  nnmord  8634  omsmo  8659  swoer  8735  unxpwdom  9586  rankxplim3  9878  cdainflem  10184  ackbij2  10240  sornom  10274  fin23lem20  10334  fpwwe2lem9  10636  inatsk  10775  ltadd2  11322  ltord1  11744  ltmul1  12068  lt2msq  12103  zle0orge1  12579  mul2lt0bi  13084  xmullem2  13248  difreicc  13465  fzospliti  13668  om2uzlti  13919  om2uzlt2i  13920  om2uzf1oi  13922  absor  15251  ruclem12  16188  dvdslelem  16256  odd2np1lem  16287  odd2np1  16288  isprm6  16655  pythagtrip  16771  pc2dvds  16816  mreexexlem4d  17595  mreexexd  17596  ablsimpgprmd  20026  irredrmul  20318  znidomb  21336  mplsubrglem  21782  ppttop  22730  filconn  23607  trufil  23634  ufildr  23655  plycj  26027  cosord  26276  logdivlt  26365  isosctrlem2  26560  atans2  26672  wilthlem2  26809  basellem3  26823  lgsdir2lem4  27067  pntpbnd1  27325  nofv  27396  nolesgn2o  27410  noetalem1  27480  mirhl  28197  axcontlem2  28490  axcontlem4  28492  ex-natded5.13-2  29936  hiidge0  30618  chirredlem4  31913  disjxpin  32086  nn0xmulclb  32251  iocinif  32259  pmtrcnelor  32522  isprmidlc  32840  rhmpreimaprmidl  32844  minplyirred  33059  erdszelem11  34490  erdsze2lem2  34493  satfv1  34652  satfdmlem  34657  fmla1  34676  satffunlem2lem2  34695  dfon2lem5  35063  btwnconn1lem14  35376  btwnconn2  35378  bj-nnford  35932  poimir  36824  ispridlc  37241  lcvexchlem4  38210  lcvexchlem5  38211  paddss1  38991  paddss2  38992  mulgt0con1dlem  41632  rexzrexnn0  41844  pell14qrdich  41909  acongsym  42017  dvdsacongtr  42025  or3or  43076  clsk1indlem3  43096  mnringmulrcld  43289  nn0eo  47301  prelrrx2b  47487  itscnhlc0xyqsol  47538  itschlc0xyqsol  47540  inlinecirc02plem  47559