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  4820  trun  5234  propeqop  5495  fr2nr  5643  sossfld  6189  ordtri3or  6400  ordelinel  6471  funun  6589  soisores  7336  sorpsscmpl  7744  ordunisuc2  7849  fnse  8138  oaord  8541  omord2  8561  omcan  8563  oeord  8583  oecan  8584  nnaord  8614  nnmord  8627  omsmo  8653  swoer  8735  unxpwdom  9561  rankxplim3  9863  cdainflem  10190  ackbij2  10244  sornom  10279  fin23lem20  10339  fpwwe2lem9  10642  inatsk  10781  ltadd2  11332  ltord1  11758  ltmul1  12083  lt2msq  12118  zle0orge1  12626  mul2lt0bi  13142  xmullem2  13309  difreicc  13529  fzospliti  13739  om2uzlti  14006  om2uzlt2i  14007  om2uzf1oi  14009  absor  15377  ruclem12  16322  dvdslelem  16392  odd2np1lem  16423  odd2np1  16424  isprm6  16798  pythagtrip  16919  pc2dvds  16964  mreexexlem4d  17728  mreexexd  17729  chnccat  18707  ablsimpgprmd  20218  irredrmul  20542  isprmidlc  21509  rhmpreimaprmidl  21516  znidomb  21748  mplsubrglem  22190  ppttop  23201  filconn  24077  trufil  24104  ufildr  24125  plycj  26471  plycjOLD  26473  cosord  26733  logdivlt  26823  isosctrlem2  27021  atans2  27133  wilthlem2  27270  basellem3  27284  lgsdir2lem4  27529  pntpbnd1  27787  nofv  27858  nolesgn2o  27872  noetalem1  27942  om2noseqlt2  28530  om2noseqf1o  28531  zcuts0  28638  mirhl  28993  axcontlem2  29352  axcontlem4  29354  ex-natded5.13-2  30804  hiidge0  31487  chirredlem4  32782  disjxpin  32970  nn0xmulclb  33153  iocinif  33163  pmtrcnelor  33442  minplyirred  34132  erdszelem11  35714  erdsze2lem2  35717  satfv1  35876  satfdmlem  35881  fmla1  35900  satffunlem2lem2  35919  pm3.48ALT  36199  dfon2lem5  36298  btwnconn1lem14  36613  btwnconn2  36615  bj-nnford  37423  poimir  38345  ispridlc  38762  lcvexchlem4  39852  lcvexchlem5  39853  paddss1  40632  paddss2  40633  mulgt0con1dlem  43284  rexzrexnn0  43572  pell14qrdich  43637  acongsym  43744  dvdsacongtr  43752  or3or  44790  clsk1indlem3  44810  mnringmulrcld  44993  grlimprclnbgrvtx  48805  nn0eo  49349  prelrrx2b  49535  itscnhlc0xyqsol  49586  itschlc0xyqsol  49588  inlinecirc02plem  49607