|   | 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 458 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: ancom 460 ancom2s 650 ancom1s 653 r19.29rOLD 3116 xpord2pred 8171 infsupprpr 9545 muladdmod 13954 fi1uzind 14547 prmgapprmolem 17100 c0snmhm 20464 mat1dimcrng 22484 dmatcrng 22509 cramerlem1 22694 cramer 22698 pmatcollpwscmatlem2 22797 uhgr3cyclex 30202 3cyclfrgrrn 30306 frgrreggt1 30413 grpoidinvlem3 30526 atomli 32402 lfuhgr3 35126 cusgredgex 35128 satfun 35417 elnanelprv 35435 arg-ax 36418 bj-prmoore 37117 cnambfre 37676 prter1 38881 prjspersym 42622 rp-oelim2 43326 tfsconcatfv2 43358 tfsconcatrn 43360 oaun3lem2 43393 mnuop3d 44295 eliuniincex 45119 eliincex 45120 dvdsn1add 45959 fourierdlem42 46169 fourierdlem80 46206 etransclem38 46292 prprelprb 47509 reupr 47514 reuopreuprim 47518 gbegt5 47753 clnbgrgrim 47907 pgrpgt2nabl 48287 | 
| Copyright terms: Public domain | W3C validator |