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  4804  propeqop  5454  fr2nr  5600  sossfld  6139  ordtri3or  6343  ordelinel  6414  funun  6532  soisores  7268  sorpsscmpl  7674  sucexeloniOLD  7750  ordunisuc2  7784  fnse  8073  oaord  8472  omord2  8492  omcan  8494  oeord  8513  oecan  8514  nnaord  8544  nnmord  8557  omsmo  8583  swoer  8663  unxpwdom  9500  rankxplim3  9796  cdainflem  10101  ackbij2  10155  sornom  10190  fin23lem20  10250  fpwwe2lem9  10552  inatsk  10691  ltadd2  11238  ltord1  11664  ltmul1  11992  lt2msq  12028  zle0orge1  12506  mul2lt0bi  13019  xmullem2  13185  difreicc  13405  fzospliti  13612  om2uzlti  13875  om2uzlt2i  13876  om2uzf1oi  13878  absor  15225  ruclem12  16168  dvdslelem  16238  odd2np1lem  16269  odd2np1  16270  isprm6  16643  pythagtrip  16764  pc2dvds  16809  mreexexlem4d  17571  mreexexd  17572  ablsimpgprmd  20014  irredrmul  20330  znidomb  21486  mplsubrglem  21929  ppttop  22910  filconn  23786  trufil  23813  ufildr  23834  plycj  26199  plycjOLD  26201  cosord  26456  logdivlt  26546  isosctrlem2  26745  atans2  26857  wilthlem2  26995  basellem3  27009  lgsdir2lem4  27255  pntpbnd1  27513  nofv  27585  nolesgn2o  27599  noetalem1  27669  om2noseqlt2  28217  om2noseqf1o  28218  mirhl  28642  axcontlem2  28928  axcontlem4  28930  ex-natded5.13-2  30378  hiidge0  31060  chirredlem4  32355  orim12da  32420  disjxpin  32550  nn0xmulclb  32727  iocinif  32737  pmtrcnelor  33046  isprmidlc  33394  rhmpreimaprmidl  33398  minplyirred  33677  erdszelem11  35173  erdsze2lem2  35176  satfv1  35335  satfdmlem  35340  fmla1  35359  satffunlem2lem2  35378  pm3.48ALT  35658  dfon2lem5  35760  btwnconn1lem14  36073  btwnconn2  36075  bj-nnford  36724  poimir  37632  ispridlc  38049  lcvexchlem4  39015  lcvexchlem5  39016  paddss1  39796  paddss2  39797  mulgt0con1dlem  42442  rexzrexnn0  42777  pell14qrdich  42842  acongsym  42949  dvdsacongtr  42957  or3or  43996  clsk1indlem3  44016  mnringmulrcld  44201  grlimprclnbgrvtx  47984  nn0eo  48514  prelrrx2b  48700  itscnhlc0xyqsol  48751  itschlc0xyqsol  48753  inlinecirc02plem  48772