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  4801  propeqop  5450  fr2nr  5596  sossfld  6138  ordtri3or  6343  ordelinel  6414  funun  6532  soisores  7267  sorpsscmpl  7673  ordunisuc2  7780  fnse  8069  oaord  8468  omord2  8488  omcan  8490  oeord  8509  oecan  8510  nnaord  8540  nnmord  8553  omsmo  8579  swoer  8659  unxpwdom  9482  rankxplim3  9781  cdainflem  10086  ackbij2  10140  sornom  10175  fin23lem20  10235  fpwwe2lem9  10537  inatsk  10676  ltadd2  11224  ltord1  11650  ltmul1  11978  lt2msq  12014  zle0orge1  12492  mul2lt0bi  13000  xmullem2  13166  difreicc  13386  fzospliti  13593  om2uzlti  13859  om2uzlt2i  13860  om2uzf1oi  13862  absor  15209  ruclem12  16152  dvdslelem  16222  odd2np1lem  16253  odd2np1  16254  isprm6  16627  pythagtrip  16748  pc2dvds  16793  mreexexlem4d  17555  mreexexd  17556  chnccat  18534  ablsimpgprmd  20031  irredrmul  20347  znidomb  21500  mplsubrglem  21942  ppttop  22923  filconn  23799  trufil  23826  ufildr  23847  plycj  26211  plycjOLD  26213  cosord  26468  logdivlt  26558  isosctrlem2  26757  atans2  26869  wilthlem2  27007  basellem3  27021  lgsdir2lem4  27267  pntpbnd1  27525  nofv  27597  nolesgn2o  27611  noetalem1  27681  om2noseqlt2  28231  om2noseqf1o  28232  mirhl  28658  axcontlem2  28945  axcontlem4  28947  ex-natded5.13-2  30398  hiidge0  31080  chirredlem4  32375  orim12da  32439  disjxpin  32570  nn0xmulclb  32758  iocinif  32768  pmtrcnelor  33067  isprmidlc  33419  rhmpreimaprmidl  33423  minplyirred  33745  erdszelem11  35266  erdsze2lem2  35269  satfv1  35428  satfdmlem  35433  fmla1  35452  satffunlem2lem2  35471  pm3.48ALT  35751  dfon2lem5  35850  btwnconn1lem14  36165  btwnconn2  36167  bj-nnford  36816  poimir  37713  ispridlc  38130  lcvexchlem4  39156  lcvexchlem5  39157  paddss1  39936  paddss2  39937  mulgt0con1dlem  42587  rexzrexnn0  42921  pell14qrdich  42986  acongsym  43093  dvdsacongtr  43101  or3or  44140  clsk1indlem3  44160  mnringmulrcld  44345  grlimprclnbgrvtx  48123  nn0eo  48653  prelrrx2b  48839  itscnhlc0xyqsol  48890  itschlc0xyqsol  48892  inlinecirc02plem  48911