com3r - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > com3r		Structured version Visualization version GIF version

Theorem com3r 87

Description: Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.)

**Hypothesis**
Ref	Expression
com3.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

**Assertion**
Ref	Expression
com3r	⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))

**Proof of Theorem com3r**
Step	Hyp	Ref	Expression
1		com3.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	com23 86	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
3	2	com12 32	1 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))

Colors of variables: wff setvar class

Syntax hints: → wi 4

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

This theorem is referenced by: com13 88 com3l 89 com14 96 expd 415 elabgt 3660 elabgtOLD 3661 mob 3712 otiunsndisj 5522 sotri2 6135 sotri3 6136 relresfld 6280 limuni3 7856 poxp 8133 soxp 8134 tz7.49 8466 omwordri 8593 odi 8600 omass 8601 oewordri 8613 nndi 8644 nnmass 8645 frr3g 9780 r1sdom 9798 tz9.12lem3 9813 cardlim 9996 carduni 10005 alephordi 10098 alephval3 10134 domtriomlem 10466 axdc3lem2 10475 axdc3lem4 10477 axcclem 10481 zorn2lem5 10524 zorn2lem6 10525 axdclem2 10544 alephval2 10596 gruen 10836 grur1a 10843 grothomex 10853 nqereu 10953 distrlem5pr 11051 psslinpr 11055 ltaprlem 11068 suplem1pr 11076 lbreu 12195 fleqceilz 13852 caubnd 15338 divconjdvds 16292 algcvga 16550 algfx 16551 gsummatr01lem3 22572 fiinopn 22816 hausnei 23245 hausnei2 23270 cmpsublem 23316 cmpsub 23317 fcfneii 23954 ppiublem1 27148 ssltun2 27755 nb3grprlem1 29206 cusgrsize2inds 29280 wlk1walk 29466 clwlkclwwlklem2 29823 clwwlkf 29870 clwwlknonwwlknonb 29929 vdgn1frgrv2 30119 frgrncvvdeqlem8 30129 frgrncvvdeqlem9 30130 frgrreggt1 30216 frgrregord013 30218 chintcli 31154 h1datomi 31404 strlem3a 32075 hstrlem3a 32083 mdexchi 32158 cvbr4i 32190 mdsymlem4 32229 mdsymlem6 32231 3jaodd 35309 ifscgr 35640 bj-fvimacnv0 36765 exrecfnlem 36858 wepwsolem 42466 rp-fakeimass 42942 ee233 43958 iccpartgt 46767 lighneal 46951 ldepspr 47541

	
		OSZAR »