Theorem ancoms 334

Description: Inference commuting conjunction in antecedent. Notational convention: We sometimes suffix with "s" the label of an inference that manipulates an antecedent, leaving the consequent unchanged. The "s" means that the inference eliminates the need for a syllogism (syl 12) -type inference in a proof.

Hypothesis

Ref	Expression
ancoms.1	⊢ ((φ ∧ ψ) → χ)

Assertion

Ref	Expression
ancoms	⊢ ((ψ ∧ φ) → χ)

Proof of Theorem ancoms

Step	Hyp	Ref	Expression
1		ancom 333	. 2 ⊢ ((ψ ∧ φ) ↔ (φ ∧ ψ))
2		ancoms.1	. 2 ⊢ ((φ ∧ ψ) → χ)
3	1, 2	sylbi 174	1 ⊢ ((ψ ∧ φ) → χ)

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  anabsi8 380  anabss4 383  sylan9bbr 419  bi2anan9r 479  mpancom 528  2exeu 1066  2eu1 1067  2eu3 1069  cleqan12rd 1117  sylan9eqr 1145  r19.21be 1269  sylan9ssr 1515  difex2 1951  breqan12rd 2075  wereu 2197  ordelssne 2225  ordtri3or 2230  ordtri2 2233  ordtri2or 2328  dfom2 2374  ordom 2382  findsg 2398  tfindsg 2402  tfindsg2 2403  weinxp 2467  dminss 2648  imainss 2649  coexg 2671  funeq 2683  funeu 2685  funco 2696  funcnvuni 2706  f1co 2783  f1o2 2804  f1ocnv 2811  f1oco 2816  fsn2 2896  fnressn 2897  fressnfv 2898  isotr 2935  isotrALT 2936  tfrlem8 2956  tfr3 2964  tz7.48-2 2995  tz7.49 2997  opreqan12rd 3016  omcl 3139  oaordi 3148  oaword 3151  oawordri 3152  oaord1 3153  oaword2 3155  oa00 3161  oalimcl 3162  oaass 3163  oen0 3165  nnarcl 3174  nnaordr 3178  nnmsucr 3182  nnmcom 3183  nnmordi 3188  omsmo 3196  ersym 3209  ecopoprsym 3246  ecoprcom 3255  mapvalg 3263  ener 3313  domtr 3320  fundmen 3333  xpdom2 3345  onomeneq 3414  nndomo 3416  isfinite1 3425  unfi 3441  infcntss 3443  fiint 3445  preleq 3454  suc11reg 3456  inf3lem5 3468  aceq3 3556  aceq5 3563  zornlem6 3608  imadomg 3616  domtri 3644  sucdom 3648  unxpdom2 3651  sdomel 3653  alephord3 3683  aleph11 3684  cardaleph 3690  ltsopi 3810  mulclpi 3815  addcompi 3816  mulcompi 3818  ltapi 3824  ltmpi 3825  ordpipq 3850  ltrpq 3879  prnmadd 3894  genpnnp 3902  addcompr 3917  mulcompr 3919  ltsopr 3930  prlem934b 3932  prlem934 3933  ltexprlem2 3937  suplem1pr 3955  suplem2pr 3956  ltsrpr 3980  ssgt0sr 4011  suppsr2 4017  axmulcl 4068  axmulass 4073  axdistr 4074  axltadd 4085  mulneg2t 4197  negdi3t 4202  mulcant2 4209  divmuldivt 4263  divdivdivt 4265  letri3t 4283  leloet 4284  lenltt 4285  lerec 4411  le2sq 4415  sq11 4416  nnmulclt 4437  nn0subt 4587  zaddclt 4590  zrevaddclt 4592  znnsubt 4595  zltp1let 4597  zneo 4601  uzwo 4605  nnwoOLD 4608  zmax 4618  zbtwnre 4619  rebtwnz 4620  flgzt 4626  qrevaddclt 4648  qbtwnre 4650  om2uzf1o 4656  expcllem 4682  nn0opth 4724  sqr2irr 4782  facclt 4874  ruclem13 4897  nn0ennn 4925  znnenlem 4929  infxpidmlem8 4940  infxpidmlem12 4944  infunabs 4946  infcdaabs 4947  infdif 4948  infxpabs 4949  infmap1 4950  infmap2lem2 4952  hvsubcan2t 5017  orthcom 5061  normpyct 5093  hlimcaui 5141  ocsh 5164  occon2t 5169  chocuni 5179  occl 5188  projlem2 5194  projlem26 5218  pjthu2 5242  pjvalt 5246  shscl 5282  shscomt 5284  shsel2t 5287  spanss 5319  shjcomt 5331  shlej1t 5356  shmods 5363  chpsscon3t 5420  spansnmul 5469  spansncol 5473  spanunsn 5482  spansncv 5542  5oalem2 5545  3oalem2 5553  strlem4 5695  strlem5 5696  cvcon3t 5716  cvnsymt 5722  mdbr2 5728  mdbr3 5729  mdbr4 5730  dmdbr 5731  dmdbr2 5733  ssmd2 5735  ssdmd1 5736  atss 5744  atcveq0 5746  atnem0 5766  atexch 5769  atcvatlem 5770  atcvat 5771  atcvat3 5774  mdsymlem3 5778  mdsymlem4 5779  mdsymlem5 5780  mdsymlem8 5783  sumdmdlem 5786

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org