Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm3.22 | Structured version Visualization version GIF version |
Description: Theorem *3.22 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Nov-2012.) |
Ref | Expression |
---|---|
pm3.22 | ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜓 ∧ 𝜑)) | |
2 | 1 | ancoms 459 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 208 df-an 397 |
This theorem is referenced by: ancom 461 ancom2s 646 ancom1s 649 r19.29r 3255 infsupprpr 8957 fi1uzind 13845 prmgapprmolem 16387 mat1dimcrng 21016 dmatcrng 21041 cramerlem1 21226 cramer 21230 pmatcollpwscmatlem2 21328 uhgr3cyclex 27889 3cyclfrgrrn 27993 frgrreggt1 28100 grpoidinvlem3 28211 atomli 30087 lfuhgr3 32264 cusgredgex 32266 satfun 32556 elnanelprv 32574 arg-ax 33662 cnambfre 34822 prter1 35897 prjspersym 39137 mnuop3d 40487 eliuniincex 41256 eliincex 41257 dvdsn1add 42104 fourierdlem42 42315 fourierdlem80 42352 etransclem38 42438 prprelprb 43526 reupr 43531 reuopreuprim 43535 gbegt5 43773 c0snmhm 44084 pgrpgt2nabl 44312 |
Copyright terms: Public domain | W3C validator |