Theorem impcom 351

Description: Importation inference with commuted antecedents.

Hypothesis

Ref	Expression
imp.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
impcom	|- ((ps /\ ph) -> ch)

Proof of Theorem impcom

Step	Hyp	Ref	Expression
1		imp.1	. . 3 |- (ph -> (ps -> ch))
2	1	com12 11	. 2 |- (ps -> (ph -> ch))
3	2	imp 350	1 |- ((ps /\ ph) -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  pm5.75 747  ax11eq 1356  ax11el 1357  a12stdy4 1368  mopick 1426  pm2.61ne 1625  gencl 1819  2gencl 1820  vtocl2gf 1840  vtocl2ga 1844  rcla4dv 1869  rcla4edv 1870  sbcbid 1966  sbc19.20dv 1975  csbeq2d 2008  minel 2314  r19.2z 2337  ssuni 2512  ssexg 2711  unipw 2746  solin 2848  reuuni1 2872  dfwe2 2925  wereu 2935  2optocl 3226  3optocl 3227  resieq 3360  funimaexg 3561  fnun 3580  fun 3626  fvopab2 3776  fnressn 3822  fressnfv 3823  funfvima3 3839  funiunfv 3851  f1fveq 3861  isotr 3882  ndmoprcl 4030  oacl 4154  omcl 4155  oecl 4156  oarec 4180  oewordri 4203  oelim2 4206  nnacl 4213  nnmcl 4214  nnecl 4215  nnmsucr 4224  oaabs 4236  ectocl 4286  2ecoptocl 4288  uniixp 4341  mapunen 4482  limensuc 4487  nneneq 4492  sucdomi 4503  preleq 4575  zfregs 4619  rankxpsuc 4687  ac6lem 4726  kmlem2 4738  fodom 4770  axrepndlem2 4917  axregndlem2 4927  axinfnd 4930  axacndlem4 4934  axacndlem5 4935  axacnd 4936  suppsr2 5195  supsrlem2 5198  negeu 5327  mulcant 5661  receu 5670  divmuldivt 5736  nnaddclt 5888  nnmulclt 5889  lbreu 5992  xrsupsslem 6023  xrinfmsslem 6024  supxrunb1 6036  supxrunb2 6037  uzwo5OLD 6159  om2uzlt 6235  seq1rn2 6258  uz11t 6364  uzaddclt 6381  seqzrn2 6488  expcllem 6507  expeq0t 6517  expord2t 6535  cjexpt 6752  absexpt 6803  ser1absdiflem 6866  faclbnd 6882  faclbnd6 6891  fsum2mul 6975  fsumcmpndx2 6980  bcxmas 7014  climconst3 7033  iserzshft2 7044  clim2serzt 7070  climcmplem 7073  cvgratlem2ALT 7183  fsum0diaglem2 7192  abscncflem 7209  ivthlem7 7222  ivthlem7OLD 7231  ef0lem 7252  efexpt 7314  demoivre 7426  acdc3 7429  acdc5 7435  znnenlem 7443  znnenlemOLD 7444  tgval3t 7567  clsss 7629  ntrss 7630  ntrss2 7632  ssnei2 7671  mettri2 7752  mettri 7756  metreslem 7762  metcni 7833  bcthlem16 7948  isgrp 7975  grplactf1o 8034  ringid 8082  ringdi 8083  ringdir 8084  ringass 8085  vcdi 8108  vcdir 8109  vcass 8110  lnolin 8349  nmosetre 8359  ubthlem10 8469  chsscm 9033  occl 9097  projlem13 9114  dfch2 9164  shscl 9196  chintcl 9210  spansncv 9514  pjrn 9564  nmopsetretALT 9707  nmfnsetret 9721  lnoplt 9754  lnfnlt 9771  nmcopexlem1 9866  nmcfnexlem1 9895  cnlnadjlem5 9919  pjss2co 10003  pjorthco 10008  pjscj 10009  pjssdif2 10013  pjclem4a 10036  pj3lem1 10044  strlem4 10091  strlem5 10092  hstrlem4 10099  hstrlem5 10100  cvmd 10159  mdslmd3 10167  atcv1t 10215  atcvat4 10232  cdj3lem2a 10268  cdj3lem3a 10271  rcla4devOLD 10331  fiiu2 10377  mapudiscn 10399  cmphmp 10408  cnvhmpha 10412  cnvhmphb 10413  hmeogrp 10425  homcard 10426  qusp 10430  iintlem1 10476  homgrf 10574  ismonc 10584  cmpmon 10585

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain