Theorem orim12d 979

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

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

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 402  df-or 862

This theorem is used by:  orim12da  980  orim1d  981  orim2d  982  3orim123d  1472  preq12b  4804  trun  5222  propeqop  5478  fr2nr  5627  sossfld  6177  ordtri3or  6395  ordelinel  6466  funun  6586  soisores  7335  sorpsscmpl  7750  ordunisuc2  7855  fnse  8152  oaord  8558  omord2  8578  omcan  8580  oeord  8600  oecan  8601  nnaord  8631  nnmord  8644  omsmo  8670  swoer  8752  unxpwdom  9586  rankxplim3  9901  cdainflem  10269  ackbij2  10323  sornom  10358  fin23lem20  10418  fpwwe2lem9  10727  inatsk  10866  ltadd2  11417  ltord1  11845  ltmul1  12170  lt2msq  12205  zle0orge1  12713  mul2lt0bi  13231  xmullem2  13398  difreicc  13618  fzospliti  13829  om2uzlti  14096  om2uzlt2i  14097  om2uzf1oi  14099  absor  15472  ruclem12  16414  dvdslelem  16484  odd2np1lem  16515  odd2np1  16516  isprm6  16895  pythagtrip  17017  pc2dvds  17062  mreexexlem4d  17826  mreexexd  17827  chnccat  18805  ablsimpgprmd  20336  irredrmul  20662  isprmidlc  21633  rhmpreimaprmidl  21640  znidomb  21872  mplsubrglem  22316  ppttop  23330  filconn  24207  trufil  24234  ufildr  24255  plycj  26601  cosord  26864  logdivlt  26954  isosctrlem2  27152  atans2  27264  wilthlem2  27401  basellem3  27415  lgsdir2lem4  27660  pntpbnd1  27918  nofv  28019  nolesgn2o  28033  noetalem1  28103  om2noseqlt2  28691  om2noseqf1o  28692  zcuts0  28799  mirhl  29156  axcontlem2  29548  axcontlem4  29550  ex-natded5.13-2  31022  hiidge0  31705  chirredlem4  33000  disjxpin  33229  nn0xmulclb  33409  iocinif  33419  pmtrcnelor  33698  minplyirred  34389  dfac16  35810  erdszelem11  36052  erdsze2lem2  36055  satfv1  36214  satfdmlem  36219  fmla1  36238  satffunlem2lem2  36257  pm3.48ALT  36537  dfon2lem5  36641  btwnconn1lem14  36957  btwnconn2  36959  bj-nnford  37751  poimir  38664  ispridlc  39097  lcvexchlem4  40187  lcvexchlem5  40188  paddss1  40967  paddss2  40968  mulgt0con1dlem  43626  rexzrexnn0  43904  pell14qrdich  43969  acongsym  44076  dvdsacongtr  44084  or3or  45116  clsk1indlem3  45136  mnringmulrcld  45319  grlimprclnbgrvtx  49190  nn0eo  49733  itscnhlc0xyqsol  49970  itschlc0xyqsol  49972