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  4802  propeqop  5447  fr2nr  5593  sossfld  6133  ordtri3or  6338  ordelinel  6409  funun  6527  soisores  7261  sorpsscmpl  7667  ordunisuc2  7774  fnse  8063  oaord  8462  omord2  8482  omcan  8484  oeord  8503  oecan  8504  nnaord  8534  nnmord  8547  omsmo  8573  swoer  8653  unxpwdom  9475  rankxplim3  9771  cdainflem  10076  ackbij2  10130  sornom  10165  fin23lem20  10225  fpwwe2lem9  10527  inatsk  10666  ltadd2  11214  ltord1  11640  ltmul1  11968  lt2msq  12004  zle0orge1  12482  mul2lt0bi  12995  xmullem2  13161  difreicc  13381  fzospliti  13588  om2uzlti  13854  om2uzlt2i  13855  om2uzf1oi  13857  absor  15204  ruclem12  16147  dvdslelem  16217  odd2np1lem  16248  odd2np1  16249  isprm6  16622  pythagtrip  16743  pc2dvds  16788  mreexexlem4d  17550  mreexexd  17551  chnccat  18529  ablsimpgprmd  20027  irredrmul  20343  znidomb  21496  mplsubrglem  21939  ppttop  22920  filconn  23796  trufil  23823  ufildr  23844  plycj  26208  plycjOLD  26210  cosord  26465  logdivlt  26555  isosctrlem2  26754  atans2  26866  wilthlem2  27004  basellem3  27018  lgsdir2lem4  27264  pntpbnd1  27522  nofv  27594  nolesgn2o  27608  noetalem1  27678  om2noseqlt2  28228  om2noseqf1o  28229  mirhl  28655  axcontlem2  28941  axcontlem4  28943  ex-natded5.13-2  30391  hiidge0  31073  chirredlem4  32368  orim12da  32432  disjxpin  32563  nn0xmulclb  32749  iocinif  32759  pmtrcnelor  33055  isprmidlc  33407  rhmpreimaprmidl  33411  minplyirred  33719  erdszelem11  35233  erdsze2lem2  35236  satfv1  35395  satfdmlem  35400  fmla1  35419  satffunlem2lem2  35438  pm3.48ALT  35718  dfon2lem5  35820  btwnconn1lem14  36133  btwnconn2  36135  bj-nnford  36784  poimir  37692  ispridlc  38109  lcvexchlem4  39075  lcvexchlem5  39076  paddss1  39855  paddss2  39856  mulgt0con1dlem  42501  rexzrexnn0  42836  pell14qrdich  42901  acongsym  43008  dvdsacongtr  43016  or3or  44055  clsk1indlem3  44075  mnringmulrcld  44260  grlimprclnbgrvtx  48029  nn0eo  48559  prelrrx2b  48745  itscnhlc0xyqsol  48796  itschlc0xyqsol  48798  inlinecirc02plem  48817