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  4810  trun  5223  propeqop  5479  fr2nr  5628  sossfld  6177  ordtri3or  6388  ordelinel  6459  funun  6578  soisores  7327  sorpsscmpl  7739  ordunisuc2  7844  fnse  8134  oaord  8539  omord2  8559  omcan  8561  oeord  8581  oecan  8582  nnaord  8612  nnmord  8625  omsmo  8651  swoer  8733  unxpwdom  9567  rankxplim3  9879  cdainflem  10247  ackbij2  10301  sornom  10336  fin23lem20  10396  fpwwe2lem9  10705  inatsk  10844  ltadd2  11395  ltord1  11823  ltmul1  12148  lt2msq  12183  zle0orge1  12691  mul2lt0bi  13209  xmullem2  13376  difreicc  13596  fzospliti  13806  om2uzlti  14073  om2uzlt2i  14074  om2uzf1oi  14076  absor  15447  ruclem12  16389  dvdslelem  16459  odd2np1lem  16490  odd2np1  16491  isprm6  16870  pythagtrip  16992  pc2dvds  17037  mreexexlem4d  17801  mreexexd  17802  chnccat  18780  ablsimpgprmd  20311  irredrmul  20637  isprmidlc  21608  rhmpreimaprmidl  21615  znidomb  21847  mplsubrglem  22291  ppttop  23305  filconn  24182  trufil  24209  ufildr  24230  plycj  26576  plycjOLD  26578  cosord  26841  logdivlt  26931  isosctrlem2  27129  atans2  27241  wilthlem2  27378  basellem3  27392  lgsdir2lem4  27637  pntpbnd1  27895  nofv  27996  nolesgn2o  28010  noetalem1  28080  om2noseqlt2  28668  om2noseqf1o  28669  zcuts0  28776  mirhl  29133  axcontlem2  29525  axcontlem4  29527  ex-natded5.13-2  30999  hiidge0  31682  chirredlem4  32977  disjxpin  33164  nn0xmulclb  33345  iocinif  33355  pmtrcnelor  33634  minplyirred  34325  erdszelem11  35935  erdsze2lem2  35938  satfv1  36097  satfdmlem  36102  fmla1  36121  satffunlem2lem2  36140  pm3.48ALT  36420  dfon2lem5  36519  btwnconn1lem14  36835  btwnconn2  36837  bj-nnford  37629  poimir  38539  ispridlc  38972  lcvexchlem4  40062  lcvexchlem5  40063  paddss1  40842  paddss2  40843  mulgt0con1dlem  43501  rexzrexnn0  43764  pell14qrdich  43829  acongsym  43936  dvdsacongtr  43944  or3or  44982  clsk1indlem3  45002  mnringmulrcld  45185  grlimprclnbgrvtx  49041  nn0eo  49584  prelrrx2b  49770  itscnhlc0xyqsol  49821  itschlc0xyqsol  49823  inlinecirc02plem  49842