Theorem impcom 349

Description: Importation inference with commuted antecedents.

Hypothesis

Ref	Expression
imp.1	⊢ (φ → (ψ → χ))

Assertion

Ref	Expression
impcom	⊢ ((ψ ⋀ φ) → χ)

Proof of Theorem impcom

Step	Hyp	Ref	Expression
1		imp.1	. . 3 ⊢ (φ → (ψ → χ))
2	1	com12 11	. 2 ⊢ (ψ → (φ → χ))
3	2	imp 348	1 ⊢ ((ψ ⋀ φ) → χ)

Syntax hints:   → wi 3   ⋀ wa 221

This theorem is referenced by:  pm5.75 754  ax11eq 1402  ax11el 1403  a12stdy4 1414  mopick 1472  pm2.61ne 1679  gencl 1874  2gencl 1875  vtocl2gf 1895  vtocl2ga 1899  rcla4dv 1924  rcla4edv 1925  sbcbid 2024  sbc19.20dv 2033  sbc2iedv 2037  csbeq2d 2069  minel 2377  r19.2z 2401  ssuni 2589  ssexg 2795  unipw 2836  solin 2936  wereu 2972  reuuni1 3106  dfwe2 3140  2optocl 3322  3optocl 3323  resieq 3463  funimaexg 3681  fnun 3700  fun 3748  fvopab2 3902  fnressn 3951  fressnfv 3952  funfvima3 3968  funiunfv 3980  f1fveq 3990  isotr 4011  ndmoprcl 4105  oacl 4306  omcl 4307  oecl 4308  oarec 4332  oewordri 4355  oelim2 4358  oeoa 4360  oeoelem 4361  oeoe 4362  nnacl 4369  nnmcl 4370  nnecl 4371  nnmsucr 4380  oaabs 4392  2ecoptocl 4445  uniixp 4498  ac6sfilem3 4590  mapunen 4649  limensuc 4654  nneneq 4659  sucdomi 4670  preleq 4748  zfregs 4793  rankxpsuc 4861  ac6lem 4900  kmlem2 4912  fodom 4944  cdaeng 5076  nnacda 5090  axrepndlem2 5099  axregndlem2 5109  axinfnd 5112  axacndlem4 5116  axacndlem5 5117  axacnd 5118  suppsr2 5377  supsrlem2 5380  negeui 5509  receui 5853  nnaddcl 6085  nnmulcl 6086  lbreu 6213  xrsupsslem 6244  xrinfmsslem 6245  supxrunb1 6257  supxrunb2 6258  uzwo5OLD 6382  uz11 6559  uzaddcl 6576  om2uzlti 6661  seq1rn2 6686  seqzrn2 6751  expcllem 6770  expeq0 6780  expord2 6801  cjexp 7018  absexp 7070  ser1absdiflem 7132  faclbnd 7148  faclbnd6 7157  fsum2mul 7240  fsumcmpndx2 7245  bcxmas 7279  climconst3 7299  iserzshft2i 7310  clim2serz 7337  climcmplem 7340  cvgratlem2ALT 7453  fsum0diaglem2 7462  abscncflem 7479  ivthlem7 7492  ef0lem 7515  efexp 7577  demoivre 7695  acdc3 7698  acdc5 7705  znnenlem 7713  tgval3 7837  clsss 7897  ntrss 7898  ntrss2 7900  ssnei2 7940  mettri2 8023  mettri 8027  metreslem 8032  metequiv 8091  metcni 8105  bcthlem16 8225  isgrp 8254  grplactf1o 8339  ringid 8386  ringdi 8388  ringdir 8389  ringass 8390  vcdi 8418  vcdir 8419  vcass 8420  vacnlem3 8584  lnolin 8669  nmosetre 8681  ubthlem10 8796  chsscmi 9388  occli 9457  projlem13 9474  dfch2 9525  shscli 9557  chintcli 9571  spansncvi 9875  pjrni 9925  nmopsetretALT 10070  nmfnsetre 10084  lnopl 10118  lnfnl 10135  nmcopexlem1 10230  nmcfnexlem1 10259  cnlnadjlem5 10283  pjss2coi 10372  pjorthcoi 10377  pjscji 10378  pjssdif2i 10382  pjclem4a 10407  pj3lem1 10415  strlem4 10462  strlem5 10463  hstrlem4 10470  hstrlem5 10471  cvmdi 10532  mdslmd3i 10540  atcv1 10589  atcvat4i 10606  cdj3lem2a 10645  cdj3lem3a 10648  f1fi 10779  xrletr2 10790  islfin 10799  bepart 10800  fiiu2 10852  lteqtpos 10880  pospos 10882  opidon 10898  grpmnd 10933  rngmgmbs3 10944  rngmgmbs4 10945  unmnd 10951  on1el3 10962  on1el4 10963  mapudiscn 11015  cmphmp 11027  cnvhmpha 11031  cnvhmphb 11032  hmeogrp 11044  homcard 11045  issubsplem1 11058  qusp 11068  rcfpfillem6 11094  sfvlim 11100  stfincomp 11122  bwt2 11123  usinuniop 11128  clindistop 11131  iintlem1 11155  homgrf 11257  ismonc 11269  cmpmon 11270  iepiclem 11278  isepic 11279  issubcat 11299  idsubfun 11312  elfiun 11421  inficlALT 11424  ordtypelem7 11433  hartog 11436  omsubsdomlem2 11441  elomsubsd 11446  subntr 11482  compsublem 11487  compsub 11488  hscptsscld 11491  alexsublem4 11499  neibastop2lem3 11582  neibastop2 11584  fnejoin2 11592  fbunfip 11631  hausfillim 11685  isfclus 11718  filnetlem1 11763  filnetlem4 11766  isga 11772  ssga 11777  gapmlem 11783  dif1card 11835  fimax 11837  welb 11851  sdclem2 11876  metf1o 11907  sstotbnd 11992  ismtycnv 12005  ismtyhmeo 12007  ismtybndlem 12008  heiborlem15 12025  heiborlem22 12032  heiborlem23 12033  heiborlem32 12042  phtpcer 12104

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 145  df-an 223

Copyright terms: Public domain