Theorem com4r 45

Description: Commutation of antecedents. Rotate right.

Hypothesis

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

Assertion

Ref	Expression
com4r	|- (th -> (ph -> (ps -> (ch -> ta))))

Proof of Theorem com4r

Step	Hyp	Ref	Expression
1		com4.1	. . 3 |- (ph -> (ps -> (ch -> (th -> ta))))
2	1	com4t 44	. 2 |- (ch -> (th -> (ph -> (ps -> ta))))
3	2	com4l 43	1 |- (th -> (ph -> (ps -> (ch -> ta))))

Syntax hints:   -> wi 3

This theorem is referenced by:  3expd 1085  uniiunlem 2693  elpwunsn 3856  onint 3876  tfindsg 3944  findsg 3980  tfrlem9 5127  tz7.49 5168  oaordi 5227  odi 5258  oaabs 5309  php 5607  fiint 5650  ee233 5837  ee33 5844  aceq6b 5904  zorn2lem6 5955  zorn2lem7 5956  carduni 6010  mulcanpi 6179  ltexprlem7 6300  xrsupsslem 7285  xrinfmsslem 7286  supxrunb1 7298  supxrunb2 7299  qbtwnre 7459  elfz4 7645  seq1rn2 7734  seqzrn2 7799  reccnv 8479  cnsscnp 9049  lmle 9238  bcthlem33 9309  ipblnfi 9857  spwmo 9999  cncomp 10331  ismnd2 10392  projlem28 10846  sumdmdlem 11990  sndw 14428  eqfnung2 14459  preotr2 14576  prltub 14602  iscnp3 14946  bwt2 14960  cmpmon 15164  cptarc 15242  cnconn 15444  inficl 15757  heiborlem11 15965  ee33VD 16703

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

Copyright terms: Public domain