Theorem 3com23 1074

Description: Commutation in antecedent. Swap 2nd and 3rd.

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 1066	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	com23 36	. 2 |- (ph -> (ch -> (ps -> th)))
4	3	3imp 1061	1 |- ((ph /\ ch /\ ps) -> th)

Syntax hints:   -> wi 3   /\ w3a 858

This theorem is referenced by:  3coml 1075  syld3an2 1144  3anidm13 1155  tfindsOLD 3943  f1ofveu 4858  curry2f 5079  nneob 5312  add23 6490  cnegexlem2 6500  subsub23 6533  subadd23 6544  addsub12 6545  mul23 6580  subsub 6627  subsub3 6628  sub23 6630  suble 6818  lesub 6819  lesubOLD 6820  ltsub23 6825  ltsub13 6826  ltleadd 6829  div13 6926  div12 6927  divdiv23 6969  qbtwnre 7459  modcyc 7516  iooval2 7534  ioo0 7535  elioo4g 7553  infmssuzle 7634  fzen 7664  shftval2 7760  exprec 7837  expcan 7846  expord 7847  exple1 7852  abs3dif 8151  climsqueeze2 8401  caucvglem6 8422  fsum0diag4 8523  acdc2lem1 8757  acdc5lem1 8760  infxpabs 8839  infxpdom 8840  infmap2 8850  cnpnei 9043  metsym 9093  metequiv 9158  metcnpi3 9170  lmnn 9213  lmuni 9229  lmle 9238  grpidinvlem2 9329  grpinvdiv 9369  gxcl 9388  nvpncan 9609  nvsub 9627  nvabs 9633  nvelbl 9657  ipval2lem2 9693  ipval2lem5 9699  ipcj 9706  iporthcom 9708  ipdi 9844  ipassr 9847  ipsubdi 9850  hlipcj 9960  fgfil 10290  extbas1 10291  hvadd23 10535  his5 10586  hoadd23 11346  hosubsub 11380  unopf1o 11477  adj2 11495  adjvalval 11498  brafnmul 11512  adjlnop 11656  leopmul2i 11706  cvntr 11864  mdsymlem5 11979  sumdmdii 11987  bnj238 12078  bnj243 12082  bnj844 12718  fseq1cl 13619  ghomf1olem 13637  divalgb 13707  mulgcdlem2 13757  elioo1t3 14846  lvsovso2 15039  idfisf 15189  inficlALT 15372  clsint2 15414  opnnei 15417  fcluscomplem 15620  ufcomp 15622  lmclim2 15850  pi1gp 16095  rngidl 16172  ispridlc 16218  pltnlt 16788  pltn2lp 16789  posgelem 16795  lubid 16807  joincomALT 16828  meetcomALT 16830  latjcom 16860  latmcom 16870  latlem12 16873  latnle 16880  latabs1 16882  lubel 16898  op0le 16916  opltcon3b 16931  cmtcomlem 16969  cmtcom 16970  cmt3 16972  cmtbr3 16975  cvrval2 16991  cvrnbtwn4 16996  leatom 17005  hlrelat1 17049  hlrelat5 17050  grpidinvlem2NEW 17110  pointpsub 17231  pmap11 17242  paddcom 17274  sspadd2 17277  paddss12 17280

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

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860

Copyright terms: Public domain