Theorem orim12d 965

Description: Disjoin antecedents and consequents in a deduction. See orim12dALT 910 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 964	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
4	1, 2, 3	syl2anc 583	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ∨ wo 846

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 847

This theorem is referenced by:  orim1d  966  orim2d  967  3orim123d  1444  preq12b  4875  propeqop  5526  fr2nr  5677  sossfld  6217  ordtri3or  6427  ordelinel  6496  funun  6624  soisores  7363  sorpsscmpl  7769  sucexeloniOLD  7846  suceloniOLD  7848  ordunisuc2  7881  fnse  8174  oaord  8603  omord2  8623  omcan  8625  oeord  8644  oecan  8645  nnaord  8675  nnmord  8688  omsmo  8714  swoer  8794  unxpwdom  9658  rankxplim3  9950  cdainflem  10257  ackbij2  10311  sornom  10346  fin23lem20  10406  fpwwe2lem9  10708  inatsk  10847  ltadd2  11394  ltord1  11816  ltmul1  12144  lt2msq  12180  zle0orge1  12656  mul2lt0bi  13163  xmullem2  13327  difreicc  13544  fzospliti  13748  om2uzlti  14001  om2uzlt2i  14002  om2uzf1oi  14004  absor  15349  ruclem12  16289  dvdslelem  16357  odd2np1lem  16388  odd2np1  16389  isprm6  16761  pythagtrip  16881  pc2dvds  16926  mreexexlem4d  17705  mreexexd  17706  ablsimpgprmd  20159  irredrmul  20453  znidomb  21603  mplsubrglem  22047  ppttop  23035  filconn  23912  trufil  23939  ufildr  23960  plycj  26337  cosord  26591  logdivlt  26681  isosctrlem2  26880  atans2  26992  wilthlem2  27130  basellem3  27144  lgsdir2lem4  27390  pntpbnd1  27648  nofv  27720  nolesgn2o  27734  noetalem1  27804  om2noseqlt2  28324  om2noseqf1o  28325  mirhl  28705  axcontlem2  28998  axcontlem4  29000  ex-natded5.13-2  30448  hiidge0  31130  chirredlem4  32425  orim12da  32487  disjxpin  32610  nn0xmulclb  32778  iocinif  32786  pmtrcnelor  33084  isprmidlc  33440  rhmpreimaprmidl  33444  minplyirred  33704  erdszelem11  35169  erdsze2lem2  35172  satfv1  35331  satfdmlem  35336  fmla1  35355  satffunlem2lem2  35374  pm3.48ALT  35654  dfon2lem5  35751  btwnconn1lem14  36064  btwnconn2  36066  bj-nnford  36717  poimir  37613  ispridlc  38030  lcvexchlem4  38993  lcvexchlem5  38994  paddss1  39774  paddss2  39775  mulgt0con1dlem  42433  rexzrexnn0  42760  pell14qrdich  42825  acongsym  42933  dvdsacongtr  42941  or3or  43985  clsk1indlem3  44005  mnringmulrcld  44197  nn0eo  48262  prelrrx2b  48448  itscnhlc0xyqsol  48499  itschlc0xyqsol  48501  inlinecirc02plem  48520