Theorem orim12d 972

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

Syntax hints:   → wi 4   ∨ wo 853

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 208  df-an 397  df-or 854

This theorem is referenced by:  orim1d  973  orim2d  974  3orim123d  1452  preq12b  4788  trun  5197  propeqop  5455  fr2nr  5602  sossfld  6144  ordtri3or  6349  ordelinel  6420  funun  6538  soisores  7278  sorpsscmpl  7684  ordunisuc2  7791  fnse  8080  oaord  8479  omord2  8499  omcan  8501  oeord  8521  oecan  8522  nnaord  8552  nnmord  8565  omsmo  8591  swoer  8672  unxpwdom  9501  rankxplim3  9803  cdainflem  10108  ackbij2  10162  sornom  10197  fin23lem20  10257  fpwwe2lem9  10560  inatsk  10699  ltadd2  11248  ltord1  11674  ltmul1  12003  lt2msq  12039  zle0orge1  12539  mul2lt0bi  13048  xmullem2  13215  difreicc  13435  fzospliti  13644  om2uzlti  13910  om2uzlt2i  13911  om2uzf1oi  13913  absor  15260  ruclem12  16206  dvdslelem  16276  odd2np1lem  16307  odd2np1  16308  isprm6  16682  pythagtrip  16803  pc2dvds  16848  mreexexlem4d  17611  mreexexd  17612  chnccat  18590  ablsimpgprmd  20090  irredrmul  20405  znidomb  21543  mplsubrglem  21985  ppttop  22997  filconn  23873  trufil  23900  ufildr  23921  plycj  26267  plycjOLD  26269  cosord  26520  logdivlt  26610  isosctrlem2  26808  atans2  26920  wilthlem2  27057  basellem3  27071  lgsdir2lem4  27316  pntpbnd1  27574  nofv  27646  nolesgn2o  27660  noetalem1  27730  om2noseqlt2  28317  om2noseqf1o  28318  zcuts0  28425  mirhl  28772  axcontlem2  29059  axcontlem4  29061  ex-natded5.13-2  30511  hiidge0  31194  chirredlem4  32489  orim12da  32552  disjxpin  32684  nn0xmulclb  32870  iocinif  32880  pmtrcnelor  33179  isprmidlc  33537  rhmpreimaprmidl  33541  minplyirred  33902  erdszelem11  35436  erdsze2lem2  35439  satfv1  35598  satfdmlem  35603  fmla1  35622  satffunlem2lem2  35641  pm3.48ALT  35921  dfon2lem5  36020  btwnconn1lem14  36335  btwnconn2  36337  bj-nnford  37107  poimir  38027  ispridlc  38444  lcvexchlem4  39536  lcvexchlem5  39537  paddss1  40316  paddss2  40317  mulgt0con1dlem  42966  rexzrexnn0  43256  pell14qrdich  43321  acongsym  43428  dvdsacongtr  43436  or3or  44474  clsk1indlem3  44494  mnringmulrcld  44679  grlimprclnbgrvtx  48497  nn0eo  49026  prelrrx2b  49212  itscnhlc0xyqsol  49263  itschlc0xyqsol  49265  inlinecirc02plem  49284