Theorem com23 72

Description: Commutation of antecedents. Swap 2nd and 3rd. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)

Hypothesis

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

Assertion

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

Proof of Theorem com23

Step	Hyp	Ref	Expression
1		com3.1	. 2 |- (ph -> (ps -> (ch -> th)))
2		pm2.27 35	. 2 |- (ch -> ((ch -> th) -> th))
3	1, 2	syl9 66	1 |- (ph -> (ch -> (ps -> th)))

Syntax hints:   -> wi 4

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

This theorem is referenced by:  com3r  73  com13  74  pm2.04  76  pm2.86d  93  impancom  427  dedlem0b  919  3com23  1157  exp3acom23  1372  ax12b  1689  a16g  1945  cbv1h  1978  sbied  2036  sbequi  2059  ax11indn  2195  eqrdav  2352  ralrimdva  2705  ralrimdvva  2710  ceqsalt  2882  vtoclgft  2906  reu6  3026  sbciegft  3077  reuss2  3536  reupick  3540  nnsucelr  4429  nndisjeq  4430  ltfintri  4467  ssfin  4471  evenodddisj  4517  nnadjoin  4521  sfintfin  4533  tfinnn  4535  spfinsfincl  4540  funssres  5145  funcnvuni  5162  fv3  5342  tz6.12-1  5345  funfvima2  5461  isoini  5498  f1o2d  5728  fnpprod  5844  enpw1  6063  enprmaplem3  6079  nclenn  6250  nchoicelem6  6295  nchoicelem12  6301  nchoicelem17  6306