Theorem ancom 266

Description: Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Wolf Lammen, 4-Nov-2012.)

Assertion

Ref	Expression
ancom	|- ( ( ph /\ ps ) <-> ( ps /\ ph ) )

Proof of Theorem ancom

Step	Hyp	Ref	Expression
1		pm3.22 265	. 2 |- ( ( ph /\ ps ) -> ( ps /\ ph ) )
2		pm3.22 265	. 2 |- ( ( ps /\ ph ) -> ( ph /\ ps ) )
3	1, 2	impbii 126	1 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )

Syntax hints:   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ancomd  267  ancomsd  269  biancomi  270  biancomd  271  pm4.71r  390  pm5.32rd  451  pm5.32ri  455  anbi2ci  459  anbi12ci  461  bianassc  470  mpan10  474  an12  561  an32  562  an13  563  an42  587  andir  820  rbaib  922  rbaibr  923  3anrot  985  3ancoma  987  excxor  1389  xorcom  1399  xordc  1403  xordc1  1404  dfbi3dc  1408  ancomsimp  1451  exancom  1619  19.29r  1632  19.42h  1698  19.42  1699  eu1  2063  moaneu  2114  moanmo  2115  2eu7  2132  eq2tri  2249  r19.28av  2626  r19.29r  2628  r19.42v  2647  rexcomf  2652  rabswap  2669  euxfr2dc  2937  rmo4  2945  reu8  2948  rmo3f  2949  rmo3  3069  incom  3342  difin2  3412  symdifxor  3416  inuni  4170  eqvinop  4258  uniuni  4466  dtruex  4573  elvvv  4704  brinxp2  4708  dmuni  4852  dfres2  4974  dfima2  4987  imadmrn  4995  imai  4999  cnvxp  5062  cnvcnvsn  5120  mptpreima  5137  rnco  5150  unixpm  5179  ressn  5184  xpcom  5190  fncnv  5297  fununi  5299  imadiflem  5310  fnres  5347  fnopabg  5354  dff1o2  5481  eqfnfv3  5631  respreima  5660  fsn  5704  fliftcnv  5812  isoini  5835  spc2ed  6252  brtpos2  6270  tpostpos  6283  tposmpo  6300  nnaord  6528  pmex  6671  elpmg  6682  mapval2  6696  mapsnen  6829  map1  6830  xpsnen  6839  xpcomco  6844  elfi2  6989  supmoti  7010  cnvti  7036  2omotaplemap  7274  elni2  7331  enq0enq  7448  prltlu  7504  prnmaxl  7505  prnminu  7506  nqprrnd  7560  ltpopr  7612  letri3  8056  lesub0  8454  creur  8934  xrletri3  9822  iooneg  10006  iccneg  10007  elfzuzb  10037  fzrev  10102  redivap  10901  imdivap  10908  rersqreu  11055  lenegsq  11122  climrecvg1n  11374  fisumcom2  11464  fsumcom  11465  fprodcom2fi  11652  fprodcom  11653  gcdcom  11992  bezoutlembi  12024  dfgcd2  12033  lcmcom  12082  isprm2  12135  unennn  12416  dfrhm2  13465  issubrng  13507  ntreq0  14016  restopn2  14067  ismet2  14238  blres  14318  metrest  14390  dedekindicclemicc  14494  sincosq3sgn  14633  lgsdi  14822