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  4831  propeqop  5487  fr2nr  5636  sossfld  6180  ordtri3or  6389  ordelinel  6460  funun  6587  soisores  7325  sorpsscmpl  7733  sucexeloniOLD  7809  suceloniOLD  7811  ordunisuc2  7844  fnse  8137  oaord  8564  omord2  8584  omcan  8586  oeord  8605  oecan  8606  nnaord  8636  nnmord  8649  omsmo  8675  swoer  8755  unxpwdom  9608  rankxplim3  9900  cdainflem  10207  ackbij2  10261  sornom  10296  fin23lem20  10356  fpwwe2lem9  10658  inatsk  10797  ltadd2  11344  ltord1  11768  ltmul1  12096  lt2msq  12132  zle0orge1  12610  mul2lt0bi  13120  xmullem2  13286  difreicc  13506  fzospliti  13713  om2uzlti  13973  om2uzlt2i  13974  om2uzf1oi  13976  absor  15324  ruclem12  16264  dvdslelem  16333  odd2np1lem  16364  odd2np1  16365  isprm6  16738  pythagtrip  16859  pc2dvds  16904  mreexexlem4d  17664  mreexexd  17665  ablsimpgprmd  20103  irredrmul  20392  znidomb  21527  mplsubrglem  21969  ppttop  22950  filconn  23826  trufil  23853  ufildr  23874  plycj  26240  plycjOLD  26242  cosord  26497  logdivlt  26587  isosctrlem2  26786  atans2  26898  wilthlem2  27036  basellem3  27050  lgsdir2lem4  27296  pntpbnd1  27554  nofv  27626  nolesgn2o  27640  noetalem1  27710  om2noseqlt2  28251  om2noseqf1o  28252  mirhl  28663  axcontlem2  28949  axcontlem4  28951  ex-natded5.13-2  30402  hiidge0  31084  chirredlem4  32379  orim12da  32444  disjxpin  32574  nn0xmulclb  32753  iocinif  32763  pmtrcnelor  33107  isprmidlc  33467  rhmpreimaprmidl  33471  minplyirred  33750  erdszelem11  35228  erdsze2lem2  35231  satfv1  35390  satfdmlem  35395  fmla1  35414  satffunlem2lem2  35433  pm3.48ALT  35713  dfon2lem5  35810  btwnconn1lem14  36123  btwnconn2  36125  bj-nnford  36774  poimir  37682  ispridlc  38099  lcvexchlem4  39060  lcvexchlem5  39061  paddss1  39841  paddss2  39842  mulgt0con1dlem  42475  rexzrexnn0  42802  pell14qrdich  42867  acongsym  42975  dvdsacongtr  42983  or3or  44022  clsk1indlem3  44042  mnringmulrcld  44227  nn0eo  48488  prelrrx2b  48674  itscnhlc0xyqsol  48725  itschlc0xyqsol  48727  inlinecirc02plem  48746