Theorem orim12d 978

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 860

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861

This theorem is used by:  orim12da  979  orim1d  980  orim2d  981  3orim123d  1471  preq12b  4814  trun  5228  propeqop  5489  fr2nr  5637  sossfld  6183  ordtri3or  6393  ordelinel  6464  funun  6582  soisores  7325  sorpsscmpl  7733  ordunisuc2  7838  fnse  8127  oaord  8530  omord2  8550  omcan  8552  oeord  8572  oecan  8573  nnaord  8603  nnmord  8616  omsmo  8642  swoer  8724  unxpwdom  9549  rankxplim3  9851  cdainflem  10178  ackbij2  10232  sornom  10267  fin23lem20  10327  fpwwe2lem9  10630  inatsk  10769  ltadd2  11320  ltord1  11746  ltmul1  12071  lt2msq  12106  zle0orge1  12614  mul2lt0bi  13130  xmullem2  13297  difreicc  13517  fzospliti  13727  om2uzlti  13993  om2uzlt2i  13994  om2uzf1oi  13996  absor  15358  ruclem12  16303  dvdslelem  16373  odd2np1lem  16404  odd2np1  16405  isprm6  16779  pythagtrip  16900  pc2dvds  16945  mreexexlem4d  17709  mreexexd  17710  chnccat  18688  ablsimpgprmd  20193  irredrmul  20516  isprmidlc  21483  rhmpreimaprmidl  21490  znidomb  21722  mplsubrglem  22164  ppttop  23175  filconn  24051  trufil  24078  ufildr  24099  plycj  26445  plycjOLD  26447  cosord  26707  logdivlt  26797  isosctrlem2  26995  atans2  27107  wilthlem2  27244  basellem3  27258  lgsdir2lem4  27503  pntpbnd1  27761  nofv  27832  nolesgn2o  27846  noetalem1  27916  om2noseqlt2  28504  om2noseqf1o  28505  zcuts0  28612  mirhl  28967  axcontlem2  29326  axcontlem4  29328  ex-natded5.13-2  30778  hiidge0  31461  chirredlem4  32756  disjxpin  32944  nn0xmulclb  33127  iocinif  33137  pmtrcnelor  33420  minplyirred  34110  erdszelem11  35701  erdsze2lem2  35704  satfv1  35863  satfdmlem  35868  fmla1  35887  satffunlem2lem2  35906  pm3.48ALT  36186  dfon2lem5  36285  btwnconn1lem14  36600  btwnconn2  36602  bj-nnford  37410  poimir  38332  ispridlc  38749  lcvexchlem4  39839  lcvexchlem5  39840  paddss1  40619  paddss2  40620  mulgt0con1dlem  43271  rexzrexnn0  43559  pell14qrdich  43624  acongsym  43731  dvdsacongtr  43739  or3or  44777  clsk1indlem3  44797  mnringmulrcld  44980  grlimprclnbgrvtx  48792  nn0eo  49336  prelrrx2b  49522  itscnhlc0xyqsol  49573  itschlc0xyqsol  49575  inlinecirc02plem  49594