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 748  ax11eq 1361  ax11el 1362  a12stdy4 1373  mopick 1431  pm2.61ne 1630  gencl 1824  2gencl 1825  vtocl2gf 1845  vtocl2ga 1849  rcla4dv 1874  rcla4edv 1875  sbcbid 1972  sbc19.20dv 1981  csbeq2d 2014  minel 2320  r19.2z 2343  ssuni 2517  ssexg 2716  unipw 2751  solin 2852  reuuni1 2877  dfwe2 2930  wereu 2940  2optocl 3231  3optocl 3232  resieq 3368  funimaexg 3567  fnun 3586  fun 3632  fvopab2 3782  fnressn 3828  fressnfv 3829  funfvima3 3845  funiunfv 3857  f1fveq 3867  isotr 3888  ndmoprcl 4036  oacl 4160  omcl 4161  oecl 4162  oarec 4186  oewordri 4209  oelim2 4212  nnacl 4219  nnmcl 4220  nnecl 4221  nnmsucr 4230  oaabs 4242  ectocl 4292  2ecoptocl 4294  uniixp 4347  mapunen 4488  limensuc 4493  nneneq 4498  sucdomi 4509  preleq 4583  zfregs 4627  rankxpsuc 4695  ac6lem 4734  kmlem2 4746  fodom 4778  axrepndlem2 4925  axregndlem2 4935  axinfnd 4938  axacndlem4 4942  axacndlem5 4943  axacnd 4944  suppsr2 5203  supsrlem2 5206  negeu 5335  mulcant 5669  receu 5678  divmuldivt 5744  nnaddclt 5896  nnmulclt 5897  lbreu 6000  xrsupsslem 6031  xrinfmsslem 6032  supxrunb1 6044  supxrunb2 6045  uzwo5OLD 6167  om2uzlt 6243  seq1rn2 6266  uz11t 6372  uzaddclt 6389  seqzrn2 6496  expcllem 6515  expeq0t 6525  expord2t 6543  cjexpt 6760  absexpt 6811  ser1absdiflem 6874  faclbnd 6890  faclbnd6 6899  fsum2mul 6983  fsumcmpndx2 6988  bcxmas 7022  climconst3 7041  iserzshft2 7052  clim2serzt 7078  climcmplem 7081  cvgratlem2ALT 7191  fsum0diaglem2 7200  abscncflem 7217  ivthlem7 7230  ivthlem7OLD 7239  ef0lem 7260  efexpt 7322  demoivre 7434  acdc3 7437  acdc5 7443  znnenlem 7451  znnenlemOLD 7452  tgval3t 7575  clsss 7637  ntrss 7638  ntrss2 7640  ssnei2 7680  mettri2 7763  mettri 7767  metreslem 7774  metcni 7846  bcthlem16 7964  isgrp 7991  grplactf1o 8049  ringid 8097  ringdi 8098  ringdir 8099  ringass 8100  vcdi 8123  vcdir 8124  vcass 8125  lnolin 8362  nmosetre 8372  ubthlem10 8482  chsscm 9051  occl 9120  projlem13 9137  dfch2 9187  shscl 9219  chintcl 9233  spansncv 9537  pjrn 9587  nmopsetretALT 9730  nmfnsetret 9744  lnoplt 9777  lnfnlt 9794  nmcopexlem1 9889  nmcfnexlem1 9918  cnlnadjlem5 9942  pjss2co 10030  pjorthco 10035  pjscj 10036  pjssdif2 10040  pjclem4a 10064  pj3lem1 10072  strlem4 10119  strlem5 10120  hstrlem4 10127  hstrlem5 10128  cvmd 10188  mdslmd3 10196  atcv1t 10244  atcvat4 10261  cdj3lem2a 10297  cdj3lem3a 10300  rcla4devOLD 10367  fiiu2 10413  mapudiscn 10435  cmphmp 10444  cnvhmpha 10448  cnvhmphb 10449  hmeogrp 10461  homcard 10462  qusp 10466  iintlem1 10512  homgrf 10610  ismonc 10620  cmpmon 10621

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