Theorem imp 350

Description: Importation inference. (The proof was shortened by Eric Schmidt, 22-Dec-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem imp

Step	Hyp	Ref	Expression
1		imp.1	. 2 ⊢ (φ → (ψ → χ))
2		impexp 347	. 2 ⊢ (((φ ⋀ ψ) → χ) ↔ (φ → (ψ → χ)))
3	1, 2	mpbir 190	1 ⊢ ((φ ⋀ ψ) → χ)

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  impcom 351  pm3.33 357  pm3.34 358  pm3.35 359  pm5.31 360  imp31 362  imp32 363  imp4b 365  imp41 368  imp42 369  imp43 370  imp44 371  imp45 372  impac 387  adantl 388  adantr 389  adantll 392  adantlr 393  adantrl 394  adantrr 395  biimpa 416  biimpar 417  biimpac 418  biimparc 419  jaob 422  jaoian 425  jaodan 426  pm4.43 431  imdistani 443  sylan 448  sylan2 451  syldan 467  sylan9r 469  anabsi7 497  3imtr3g 551  ordi 595  jcad 599  orcanai 689  mpanl1 705  mpanl2 706  mpanr1 708  mpanr2 709  mpanlr1 710  pm4.82 738  3adantl1 802  3adantl2 803  3adantl3 804  3jcad 819  3expia 834  3an1rs 844  3imp1 845  3imp2 847  syl3anl1 871  syl3anl2 872  syl3anl3 873  3anidm12 880  3anidm23 882  3jaoian 887  3jaodan 888  mp3anl1 908  mp3anl2 909  mp3anl3 910  19.21ad 1057  19.26 1065  equtr2 1131  equs4 1148  dvelimfALT 1151  a4imt 1156  a4imed 1159  equvini 1166  equs5a 1195  ax11v2 1213  ax11b 1218  dfsb2 1223  hbsb4 1246  dvelimdf 1249  sbcom 1256  equvin 1273  dvelimALT 1351  ax11eq 1361  ax11el 1362  ax11indi 1365  ax11indalem 1366  ax11inda2ALT 1367  ax11inda 1369  a12stdy2 1371  a12lem1 1374  mopick 1431  moexex 1436  nelneq 1558  nelneq2 1559  r19.21advv 1718  r19.21bi 1722  r19.23ai 1739  r19.23advv 1746  r19.15 1750  rcla4va 1871  reu3 1927  ra4sbca 1994  ra4esbca 1995  csbexg 2004  ra4csbela 2038  ssel2 2060  sstr 2068  sspsstr 2147  psssstr 2148  neldif 2161  reuss2 2271  reupick 2275  ssne0 2301  ssdisj 2314  disjpss 2315  disjssun 2322  pssdifn0 2325  dedth2h 2383  dedth4h 2385  sspr 2471  prel12 2480  iineq2 2574  ssiun 2587  dtruALT 2743  pwssun 2822  poirr 2840  potr 2841  reuuni2f 2878  mouniss 2885  elpwunsn 2907  frirr 2919  wefrc 2938  wereu 2940  ordelss 2959  trssord 2960  nordeq 2962  ordelord 2965  tz7.7 2968  ordsseleq 2971  onfr 2981  ordtr2 2997  oninton 3007  oneqmini 3012  limelon 3027  trsuc 3050  ordsssuc2 3054  unizlim 3108  limuni3 3118  tfi 3121  limomss 3132  ordom 3136  peano5 3148  findsg 3152  tfinds 3156  tfindsg 3157  tfindsg2 3158  brrelex 3202  optocl 3230  elrel 3248  relop 3270  opelxpex2 3274  breldmg 3311  elreldm 3333  relimasn 3417  asymref2 3432  funopg 3539  funssres 3544  fununi 3555  funimass2 3565  fneu 3584  fnun 3586  fss 3626  fco 3627  opelf 3631  f1oun 3697  f1dmex 3701  fv3 3724  funopfvg 3743  fvelima 3755  fvelimab 3756  fvco 3765  fvco2 3766  fvopab3ig 3769  elrnopabg 3791  dff2 3808  funfvima2 3844  funfvima3 3845  isorel 3885  isocnv 3887  isotr 3888  isotrALT 3889  isomin 3890  isoini 3891  isofrlem 3892  f1oweALT 3897  tfrlem2 3903  tfrlem7 3908  tfrlem8 3909  tfrlem9 3910  tfrlem11 3912  tfr3 3917  rdglimt 3939  tz7.49 3950  abianfp 3953  ndmoprgOLD 4035  ndmoprcl 4036  1stdm 4099  oevn0 4144  oaordi 4170  oawordeu 4179  oawordexr 4180  oalimcl 4184  oaass 4185  oarec 4186  omordi 4187  omcan 4190  omwordri 4193  omword1 4194  omlimcl 4199  odi 4200  omass 4201  oeordi 4204  oecan 4206  oewordi 4208  oewordri 4209  oeordsuc 4211  nnacom 4223  nnmcom 4231  oaabs 4242  omsmolem 4246  omsmo 4247  ecoptocl 4293  eceqopreq 4303  th3qlem1 4304  th3qlem2 4305  f1oen2g 4381  en3d 4388  dom2d 4391  fundmen 4415  undom 4424  xpdom2 4428  pw2en 4432  sbthlem1 4433  ensdomtr 4457  domsdomtr 4462  enen1 4463  enen2 4464  domen1 4465  domen2 4466  sdomen1 4467  sdomen2 4468  fodomr 4469  mapenlem2 4476  mapen 4477  mapdom2 4480  mapunen 4488  nneneq 4498  php 4499  php3 4501  finsucdom 4512  pssinf 4513  isfinite1 4516  infsdomnn 4517  pssnn 4519  ssfi 4521  domfi 4522  unblem3 4525  isfinite2 4529  unfilem1 4530  unifi 4538  fiint 4540  abfii4 4544  fodomfi 4546  fodomfib 4547  pm54.43 4552  supmo 4556  supnub 4562  suppr 4570  suc11reg 4585  inf3lem1 4593  inf3lem5 4597  inf3lem6 4598  unbnnt 4619  zfregs 4627  setind 4628  r1ord 4635  r1val1 4638  tz9.12lem3 4641  rankr1 4654  ssrankr1 4656  rankxplim3 4694  rankxpsuc 4695  aceq3 4713  aceq5lem4 4718  aceq5 4720  aceq6b 4722  ac6s 4736  numthlem 4763  zorn2lem1 4768  zorn2lem4 4771  zorn2lem5 4772  zorn2lem6 4773  zorn2lem7 4774  fodomb 4780  unidom 4788  uniimadom 4790  sucdom 4822  unxpdomlem 4823  cardlim 4831  ondomon 4836  carduni 4838  alephordi 4854  alephle 4864  cardaleph 4865  cardinfima 4871  alephval2 4882  alephval3 4883  cflim 4889  axrepndlem1 4924  axrepndlem2 4925  axrepnd 4926  axpowndlem4 4932  axinfndlem1 4937  axacndlem4 4942  axacndlem5 4943  axacnd 4944  mulclpi 5001  mulcanpi 5007  ltmpi 5011  indpi 5014  ltaddpq 5059  ltrpq 5065  elprpq 5075  prcdpq 5077  distrlem4pr 5110  psslinpr 5115  prlem934a 5117  prlem934 5119  ltaddpr 5120  ltexprlem3 5124  ltexprlem5 5126  ltaprlem 5130  prlem936 5135  suplem1pr 5141  mulcmpblnr 5163  recexsrlem 5192  mulgt0sr 5194  ssgt0sr 5197  suppsrlem 5201  suppsr2 5203  suppsr3 5204  suprelem 5239  axrrecex 5264  cnegextlem1 5325  cnegextlem2 5326  addcan 5331  renegcl 5396  letrt 5506  xrletrt 5545  xrret 5550  xrre2t 5551  addgegt0 5582  msqgt0t 5597  gt0ne0t 5600  addgt0t 5628  addgegt0t 5629  addge0t 5631  mulge0t 5660  recext 5665  mulcan 5667  mulcan2t 5670  divmult 5684  recne0t 5703  recidt 5706  div23t 5713  div13t 5714  div12t 5715  divdirt 5721  divmuldivt 5744  divadddivt 5748  divdivdivt 5749  redivcl 5762  prodgt0 5783  prodge0 5784  prodgt0t 5790  prodgt02t 5791  prodge0t 5792  prodge02t 5793  ltmul1t 5794  ltmul12it 5805  lemul12itOLD 5807  mulgt1t 5809  ltdiv1t 5813  lediv1t 5814  ltmuldivt 5825  ltmuldiv2t 5826  ltdivmult 5827  ledivmult 5828  lemuldiv2t 5833  ltrect 5840  lerect 5841  lt2msqt 5842  lediv12it 5852  le2msqt 5859  ledivp1t 5861  ledivp1 5862  ltdivp1 5863  lt1nnn 5903  nnleltp1t 5909  nndivtrt 5915  lble 6002  sup2 6006  suprub 6011  suprlub 6012  suprnub 6013  suprleub 6014  infmrcl 6024  xrsupsslem 6031  xrinfmsslem 6032  xrub 6035  supxr 6036  supxrre 6038  supxrun 6040  supxrunb1 6044  supxrunb2 6045  supxrbnd 6046  supxrub 6053  supxrleub 6054  dfn2 6067  lt0nnn0 6071  nnnn0addclt 6080  elnnz 6100  elnnz1 6110  nn0subt 6116  zaddclt 6120  zmulclt 6135  zltp1let 6136  btwnnzt 6147  zneo 6155  zneoOLD 6156  uzind2 6162  uzindOLD 6164  uzwo4OLD 6166  nn0ind-raph 6170  zbtwnre 6177  qaddclt 6215  qmulclt 6217  qrecclt 6219  qbtwnre 6224  qsqueeze 6226  rpmulclt 6236  monoord 6239  seq1rn2 6266  ser1add2 6283  ser1add 6284  iooss1 6318  iooss2 6319  elioo4g 6326  iccsupr 6339  icoshft 6349  icounlem 6353  icoun 6354  eluzt 6366  uz11t 6372  eluzp1m1t 6373  uzwo 6395  uzwoOLD 6396  elfzel2g 6420  elfz2nn0t 6435  elfz3nn0t 6437  fznn0subt 6438  fsequb 6463  fsequb2 6464  fseqsupcl 6465  fseqsupub 6466  seqzfveq 6494  seqzrn2 6496  expp1t 6514  expordit 6539  expcant 6540  expordt 6541  expword2it 6544  exple1t 6546  expubndt 6547  sq11t 6568  sq01t 6590  expnbndt 6593  sqr0 6610  sqrlem12 6622  sqrclt 6648  sqrgt0t 6649  sqrge0t 6650  sqrlet 6651  sqr00t 6652  sqrsqt 6660  sqsqrt 6661  crulem 6674  replimt 6700  absrpclt 6798  absidt 6805  absnidt 6806  leabst 6807  abssubne0t 6828  seq1bnd 6855  cau2 6858  cau5i 6862  cvg3 6868  caubnd 6871  faclbnd 6890  faclbnd4lem4 6896  bccl2t 6917  climcl 6924  sumeq2 6931  fsum1s 6955  fsum1s2 6956  fsump1s 6959  fsumcllem 6960  fsum1ps 6964  fsumsplit 6966  fsumadd 6968  fsumcom 6974  fsumrev 6975  fsumshftm 6978  fsummulc1 6979  fsummulc2 6980  fsumdivc 6981  fsumdivcALT 6982  fsumconst 6984  fsumcmp 6986  fsumcmpndx2 6988  fsumabs 6989  clm3 7025  clm4le 7027  clm0 7029  clm0nns 7031  clmi2at 7037  climconst 7039  climunii 7043  2climnn 7047  2climnn0 7048  climshft 7049  iserzshft2 7052  climge0 7057  climaddc1 7062  climaddc2 7063  climmullem4 7067  climmullem5 7068  climmulc2 7073  climsubc2 7075  clim2serzt 7078  climcmplem 7081  climserzle 7091  climcau 7100  caucvglem2 7102  caucvglem6 7106  caucvg 7107  serzf0 7113  ser1f0 7114  ser1cmp2 7121  cvgcmp3cetlem1 7132  cvgcmp3cetlem2 7133  cvgcmp3cet 7134  isumclim2tf 7141  isumclt 7152  iserzgt0 7154  isumcmpi 7158  reccnv 7161  infcvglem3 7166  expcnv 7176  georeclim 7183  geoisumr 7186  cvgratlem2ALT 7191  cvgratlem3ALT 7192  cvgratlem1 7193  cvgratlem2 7194  cvgratlem3 7195  cvgratlem5 7197  fsum0diaglem2 7200  fsum0diag3 7203  fsum0diag4 7204  elcncf 7208  elcncf1d 7213  ivthlem9 7232  efaddlem23 7310  eftlext 7328  reeff1o 7376  xpnnen 7449  znnen 7453  unbenlem 7455  infpnlem1 7457  infxpidmlem7 7509  infxpidmlem10 7512  infxpidmlem11 7513  infmap2lem1 7529  alephexp1 7534  uniopnt 7548  tgclt 7574  tgss2t 7587  basgen2t 7589  subbas2 7595  subtop 7596  fctop 7600  cctop 7602  retopbas 7605  ntrval 7626  iincld 7629  clsval2 7635  0ntr 7652  elcls 7654  elcls3 7661  neii1 7671  neii2 7672  0nnei 7676  islp2 7697  clslp 7698  qdensere 7701  cnima 7717  cnclima 7721  cnsscnp 7722  cncnplem4 7727  cncnp 7728  metxplem3 7780  metxplem4 7785  metxp 7786  rnblssm 7803  blss 7805  ssbl 7807  opnuni 7820  opnin 7821  rnblopn 7826  metcnp 7839  metcn 7841  metcnpi3 7844  metcnpi4 7845  metcni2 7847  metcnss2 7851  metdnsconst 7853  cncfmet 7857  lmnn 7887  caun0 7896  lmsslem 7903  caussi 7905  metelcls 7916  metcnp4 7920  metcn4i 7922  xplmi 7923  xplm 7925  xpcn 7926  iscms2lem3 7941  iscms2lem4 7942  iscms2lem5 7943  lmcau 7946  cmsss 7947  bcthlem2 7950  bcthlem10 7958  bcthlem21 7969  bcthlem25 7973  bcthlem28 7976  bcthlem33 7981  bcth 7982  grpass 7997  grpidinvlem3 8000  grpidinvlem4 8001  grpid 8015  grpasscan1 8027  grpnnncan2 8043  grplactf1o 8049  subgabl 8075  ghgrpilem2 8086  nvz 8249  nvcni 8279  nvlmle 8281  sspmval 8339  sspival 8344  sspimsval 8346  nmoub3i 8381  nmobndseqi 8385  nmlno0lem 8398  nmlnoubi 8401  nmblolbi 8404  isblo3i 8405  blocni 8409  ipasslem1 8434  ipasslem5 8438  ipdir 8446  ipass 8449  ipsubdir 8452  sspph 8459  ubthlem5 8477  ubthlem14 8486  ubthi 8488  htthlem7 8569  htthlem10 8572  htthlem12 8574  psref 8592  spwmo 8598  efifolem2 8657  shftefif1olem 8680  eff1i 8683  normpyct 8952  shelt 9019  shsubcltOLD 9029  chelt 9039  hlimcaui 9045  ocorth 9103  shorth 9107  ocnelt 9109  occl 9120  projlem13 9137  projlem15 9139  projlem26 9150  projlem27 9151  projlem28 9152  pjthlem13 9169  pjtheut 9174  pjpj0 9193  pjomlt 9207  shscl 9219  shsel1t 9223  chintcl 9233  shlej1t 9293  shmods 9300  shmod 9301  h1dn0 9413  spansn 9419  spansnmul 9426  spansnsst 9434  elspansn4t 9436  h1datom 9444  cm2jt 9503  osumlem4 9521  osumlem6 9523  spansncv 9537  5oalem6 9544  pjige0t 9576  pjsumt 9595  pjds 9597  pjds3 9598  homco1t 9667  homulasst 9668  eigret 9701  eigortht 9704  nmopub2tALT 9773  nmfnleub2t 9789  elnlfn2t 9792  kbpjt 9819  homco2t 9840  nmlnop0ALT 9858  nmopunt 9877  nmbdoplbt 9888  nmcopexlem1 9889  nmcopexlem6 9894  nmcoplbt 9898  nmcfnexlem1 9918  nmcfnexlem6 9923  nmcfnlbt 9927  nlelch 9932  branmfnt 9976  bra11 9979  cnvbravalt 9981  leopaddt 10003  leopmulit 10004  leopmul2it 10006  leoptrt 10008  pjnmop 10013  pjnormss 10034  pjclem4 10065  pj3s 10073  hstel2t 10084  hst1ht 10092  stle 10105  stles 10106  stadd 10111  stadd3 10113  strlem3a 10117  hstrlem3a 10125  stcltrlem1 10141  spansncv2t 10158  mdslmd1lem3 10191  mdslmd1lem4 10192  csmdsym 10198  mdexch 10199  atss 10210  atsseq 10211  superpos 10218  chcv1t 10219  chjatom 10221  hatomict 10224  hatomistic 10226  cvbr3 10231  atcv1t 10244  atexcht 10245  atoml 10246  atoml2 10247  atcvatlem 10249  atcvat 10250  atcvat2 10251  irredlem3 10256  irredlem4 10257  atcvat3 10260  atcvat4 10261  mdsymlem3 10269  sumdmdi 10278  sumdmdlem 10281  sumdmdlem2 10282  dmdbr5at 10284  cdj1 10294  cdj3lem1 10295  cdj3lem2b 10298  ghomgsg 10329  ghomf1olem 10330  findabrcl 10352  ee7.2a 10361  uninqs 10378  infi1 10383  ficli 10404  f2imacnv 10406  oooeqim2 10407  cdrci 10417  truni1 10422  esnnei 10431  hmeomap 10441  hmeocna 10442  hmeocnb 10443  cmphmp 10444  cnvhmpha 10448  cnvhmphb 10449  hmphre 10453  hmphtr 10454  hmeogrp 10461  homcard 10462  qusp 10466  filint 10473  fipfil2 10475  fgsb 10480  efilcp 10481  infi 10484  fgsb2 10485  efilcp2 10486  cnfilca 10487  iintlem1 10512  trnij 10517  idosd 10557  rdmob 10561  cmpasso 10586  cmpassoh 10609  homgrf 10610  imonclem 10619  ismonc 10620  cmpmon 10621  icmpmon 10623  idmon 10624

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