Theorem 3com23 1159

Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)

Hypothesis

Ref	Expression
3exp.1	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
3com23	|- ( ( ph /\ ch /\ ps ) -> th )

Proof of Theorem 3com23

Step	Hyp	Ref	Expression
1		3exp.1	. . . 4 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3exp 1152	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 74	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	3imp 1147	1 |- ( ( ph /\ ch /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ w3a 936

This theorem is referenced by:  3coml  1160  syld3an2  1231  3anidm13  1242  eqreu  3086  curry2f  6401  f1ofveu  6543  dfsmo2  6568  nneob  6854  f1oeng  7085  suppr  7429  infdif  8045  axdclem2  8356  gchen1  8456  grumap  8639  grudomon  8648  mul32  9189  add32  9236  subsub23  9266  subadd23  9273  addsub12  9274  subsub  9287  subsub3  9289  sub32  9291  suble  9462  lesub  9463  ltsub23  9464  ltsub13  9465  ltleadd  9467  div32  9654  div13  9655  div12  9656  divdiv32  9678  cju  9952  infmssuzle  10514  ioo0  10897  ico0  10918  ioc0  10919  icc0  10920  fzen  11028  modcyc  11231  expgt0  11368  expge0  11371  expge1  11372  shftval2  11845  abs3dif  12090  divalgb  12879  submrc  13808  mrieqv2d  13819  pltnlt  14380  pltn2lp  14381  lubid  14394  joincomALT  14413  meetcomALT  14415  tosso  14420  latjcom  14443  latmcom  14459  latnle  14469  latabs1  14471  lubel  14504  ipopos  14541  grpinvcnv  14814  mulgneg2  14872  oppgmnd  15105  oddvdsnn0  15137  oddvds  15140  odmulg  15147  odcl2  15156  lsmcomx  15426  rngcom  15647  mulgass2  15665  opprrng  15691  irredrmul  15767  irredlmul  15768  isdrngrd  15816  islmodd  15911  lmodcom  15945  opprdomn  16316  zntoslem  16792  ipcl  16819  rintopn  16937  opnnei  17139  restin  17184  cnpnei  17282  cnprest  17307  ordthaus  17402  kgen2ss  17540  hausflim  17966  fclsfnflim  18012  cnpfcf  18026  opnsubg  18090  cuspcvg  18284  psmetsym  18294  xmetsym  18330  ngpdsr  18604  ngpds2r  18606  ngpds3r  18608  clmmulg  19071  iscau2  19183  dgr1term  20131  cxpeq0  20522  cxpge0  20527  grpoidinvlem2  21746  grpoinvdiv  21786  gxcl  21806  nvpncan  22091  nvsub  22109  nvabs  22115  nvelbl  22138  ipval2lem2  22153  ipval2lem5  22159  dipcj  22166  diporthcom  22168  dipdi  22297  dipassr  22300  dipsubdi  22303  hlipcj  22366  hvadd32  22489  hvsub32  22500  his5  22541  hoadd32  23239  hosubsub  23273  unopf1o  23372  adj2  23390  adjvalval  23393  adjlnop  23542  leopmul2i  23591  cvntr  23748  mdsymlem5  23863  sumdmdii  23871  supxrnemnf  24080  tosglb  24145  unitdivcld  24252  ghomf1olem  25058  gcd32  25318  cgrrflx  25825  cgrcom  25828  cgrcomr  25835  btwntriv1  25854  cgr3com  25891  colineartriv2  25906  segleantisym  25953  seglelin  25954  btwnoutside  25963  clsint2  26222  heibor1  26409  rngoidl  26524  ispridlc  26570  nerabdioph  26759  monotoddzzfi  26895  fzneg  26937  jm2.19lem2  26951  elfzmlbm  27977  reccot  28215  bnj605  28984  bnj607  28993  op0le  29669  opltcon3b  29687  cmtcomlemN  29731  cmtcomN  29732  cmt3N  29734  cmtbr3N  29737  cvrval2  29757  cvrnbtwn4  29762  leatb  29775  atl0le  29787  atlrelat1  29804  hlatlej2  29858  hlateq  29881  hlrelat5N  29883  snatpsubN  30232  pmap11  30244  paddcom  30295  sspadd2  30298  paddss12  30301  cdleme51finvN  31038  cdleme51finvtrN  31040  cdlemeiota  31067  cdlemg2jlemOLDN  31075  cdlemg2klem  31077  cdlemg4b1  31091  cdlemg4b2  31092  trljco2  31223  tgrpabl  31233  tendoplcom  31264  cdleml6  31463  erngdvlem3-rN  31480  dia11N  31531  dib11N  31643  dih11  31748

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938