Theorem orim12d 835

Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)

Hypotheses

Ref	Expression
orim12d.1	|- ( ph -> ( ps -> ch ) )
orim12d.2	|- ( ph -> ( th -> ta ) )

Assertion

Ref	Expression
orim12d	|- ( ph -> ( ( ps \/ th ) -> ( ch \/ ta ) ) )

Proof of Theorem orim12d

Step	Hyp	Ref	Expression
1		orim12d.1	. 2 |- ( ph -> ( ps -> ch ) )
2		orim12d.2	. 2 |- ( ph -> ( th -> ta ) )
3		pm3.48 830	. 2 |- ( ( ( ps -> ch ) /\ ( th -> ta ) ) -> ( ( ps \/ th ) -> ( ch \/ ta ) ) )
4	1, 2, 3	syl2anc 661	1 |- ( ph -> ( ( ps \/ th ) -> ( ch \/ ta ) ) )

Syntax hints:   -> wi 4   \/ wo 368

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 185  df-or 370  df-an 371

This theorem is referenced by:  orim1d  836  orim2d  837  3orim123d  1302  preq12b  4195  prel12  4196  fr2nr  4850  ordtri3or  4903  sossfld  5445  funun  5621  soisores  6202  sorpsscmpl  6566  suceloni  6619  ordunisuc2  6650  fnse  6890  oaord  7186  omord2  7206  omcan  7208  oeord  7227  oecan  7228  nnaord  7258  nnmord  7271  omsmo  7293  swoer  7329  unxpwdom  8004  rankxplim3  8288  cdainflem  8560  ackbij2  8612  sornom  8646  fin23lem20  8706  fpwwe2lem10  9006  inatsk  9145  ltadd2  9677  ltord1  10068  ltmul1  10381  lt2msq  10418  xmullem2  11446  difreicc  11641  fzospliti  11814  om2uzlti  12017  om2uzlt2i  12018  om2uzf1oi  12020  absor  13083  ruclem12  13824  dvdslelem  13878  odd2np1lem  13893  odd2np1  13894  isprm6  14098  pythagtrip  14206  pc2dvds  14250  mreexexlem4d  14891  mreexexd  14892  irredrmul  17133  mplsubrglem  17864  mplsubrglemOLD  17865  znidomb  18360  ppttop  19267  filcon  20112  trufil  20139  ufildr  20160  plycj  22401  cosord  22645  logdivlt  22727  isosctrlem2  22874  atans2  22983  wilthlem2  23064  basellem3  23077  lgsdir2lem4  23322  pntpbnd1  23492  ncolne2  23713  axcontlem2  23937  axcontlem4  23939  ex-natded5.13-2  24800  hiidge0  25677  chirredlem4  26974  ifbieq12d2  27080  disjxpin  27106  mul2lt0bi  27223  iocinif  27246  erdszelem11  28271  erdsze2lem2  28274  dfon2lem5  28782  trpredrec  28884  nofv  28980  btwnconn1lem14  29313  btwnconn2  29315  ispridlc  30057  rexzrexnn0  30328  pell14qrdich  30396  acongsym  30505  dvdsacongtr  30513  lcvexchlem4  33709  lcvexchlem5  33710  paddss1  34488  paddss2  34489