Theorem com13 33

Description: Commutation of antecedents. Swap 1st and 3rd.

Hypothesis

Ref	Expression
com3.1	|- (ph -> (ps -> (ch -> th)))

Assertion

Ref	Expression
com13	|- (ch -> (ps -> (ph -> th)))

Proof of Theorem com13

Step	Hyp	Ref	Expression
1		com3.1	. . . 4 |- (ph -> (ps -> (ch -> th)))
2	1	com12 11	. . 3 |- (ps -> (ph -> (ch -> th)))
3	2	com23 32	. 2 |- (ps -> (ch -> (ph -> th)))
4	3	com12 11	1 |- (ch -> (ps -> (ph -> th)))

Syntax hints:   -> wi 3

This theorem is referenced by:  com3l 34  com14 38  ancom13s 487  ancom31s 490  ordsssuc2 3049  peano5 3143  funopg 3533  isomin 3884  abianfp 3947  omordi 4181  brecop 4290  isfinite2 4523  fiint 4534  aceq5 4712  aceq6b 4714  carduni 4830  mulgt0sr 5186  squeeze0 5872  xrsupsslem 6023  xrinfmsslem 6024  supxrunb1 6036  supxrunb2 6037  zmax 6168  facwordit 6881  infxpidmlem7 7501  infxpidmlem12 7506  cnpco 7708  iscncl 7709  cncnplem4 7716  opnin 7809  lmle 7895  bcthlem1 7933  bcthlem28 7960  bcthlem33 7965  spwmo 8580  projlem15 9116  projlem26 9127  shmods 9277  kbass6t 9966  mdsymlem6 10243  mdsymlem7 10244  cdj3lem2a 10268  cdj3lem3a 10271  uninqs 10342  fiiu 10350  11st22nd 10354  cdrci 10381  fipfil2 10439  efilcp 10445  filint2 10446  efilcp2 10450  cnfilca 10451  iintlem1 10476  cmpassoh 10573  ismonc 10584  cmpmon 10585  icmpmon 10587

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

Copyright terms: Public domain