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 749  ax11eq 1363  ax11el 1364  a12stdy4 1375  mopick 1433  pm2.61ne 1632  gencl 1826  2gencl 1827  vtocl2gf 1847  vtocl2ga 1851  rcla4dv 1876  rcla4edv 1877  sbcbid 1974  sbc19.20dv 1983  csbeq2d 2016  minel 2322  r19.2z 2345  ssuni 2520  ssexg 2719  unipw 2754  solin 2855  reuuni1 2880  dfwe2 2933  wereu 2943  2optocl 3234  3optocl 3235  resieq 3374  funimaexg 3573  fnun 3592  fun 3639  fvopab2 3789  fnressn 3835  fressnfv 3836  funfvima3 3852  funiunfv 3864  f1fveq 3874  isotr 3895  ndmoprcl 4042  oacl 4168  omcl 4169  oecl 4170  oarec 4194  oewordri 4217  oelim2 4220  nnacl 4227  nnmcl 4228  nnecl 4229  nnmsucr 4238  oaabs 4250  ectocl 4300  2ecoptocl 4302  uniixp 4355  mapunen 4496  limensuc 4501  nneneq 4506  sucdomi 4517  preleq 4591  zfregs 4635  rankxpsuc 4703  ac6lem 4742  kmlem2 4754  fodom 4786  axrepndlem2 4933  axregndlem2 4943  axinfnd 4946  axacndlem4 4950  axacndlem5 4951  axacnd 4952  suppsr2 5211  supsrlem2 5214  negeu 5343  mulcant 5675  receu 5684  divmuldivt 5751  nnaddclt 5908  nnmulclt 5909  lbreu 6013  xrsupsslem 6044  xrinfmsslem 6045  supxrunb1 6057  supxrunb2 6058  uzwo5OLD 6179  om2uzlt 6262  seq1rn2 6285  uz11t 6392  uzaddclt 6409  seqzrn2 6516  expcllem 6535  expeq0t 6545  expord2t 6564  cjexpt 6775  absexpt 6826  ser1absdiflem 6887  faclbnd 6903  faclbnd6 6912  fsum2mul 6995  fsumcmpndx2 7000  bcxmas 7034  climconst3 7054  iserzshft2 7065  clim2serzt 7092  climcmplem 7095  cvgratlem2ALT 7206  fsum0diaglem2 7215  abscncflem 7232  ivthlem7 7245  ef0lem 7268  efexpt 7330  demoivre 7441  acdc3 7444  acdc5 7450  znnenlem 7458  tgval3t 7582  clsss 7644  ntrss 7645  ntrss2 7647  ssnei2 7687  mettri2 7770  mettri 7774  metreslem 7779  metcni 7851  bcthlem16 7971  isgrp 7998  grplactf1o 8055  ringid 8102  ringdi 8103  ringdir 8104  ringass 8105  vcdi 8128  vcdir 8129  vcass 8130  lnolin 8372  nmosetre 8384  ubthlem10 8495  chsscm 9067  occl 9136  projlem13 9153  dfch2 9204  shscl 9236  chintcl 9250  spansncv 9552  pjrn 9602  nmopsetretALT 9745  nmfnsetret 9759  lnoplt 9793  lnfnlt 9810  nmcopexlem1 9906  nmcfnexlem1 9935  cnlnadjlem5 9959  pjss2co 10047  pjorthco 10052  pjscj 10053  pjssdif2 10057  pjclem4a 10081  pj3lem1 10089  strlem4 10136  strlem5 10137  hstrlem4 10144  hstrlem5 10145  cvmd 10206  mdslmd3 10214  atcv1t 10262  atcvat4 10279  cdj3lem2a 10318  cdj3lem3a 10321  fiiu2 10432  mapudiscn 10454  cmphmp 10463  cnvhmpha 10467  cnvhmphb 10468  hmeogrp 10480  homcard 10481  qusp 10485  rcfpfillem6 10512  iintlem1 10544  homgrf 10642  ismonc 10652  cmpmon 10653

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