Theorem imp 418

Description: Importation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem imp

Step	Hyp	Ref	Expression
1		df-an 360	. 2 |- ((ph /\ ps) <-> -. (ph -> -. ps))
2		imp.1	. . 3 |- (ph -> (ps -> ch))
3	2	impi 140	. 2 |- (-. (ph -> -. ps) -> ch)
4	1, 3	sylbi 187	1 |- ((ph /\ ps) -> ch)

Syntax hints:  -. wn 3   -> wi 4   /\ wa 358

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

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  impcom  419  imp3a  420  imp31  421  imp32  422  expdimp  426  impancom  427  con3and  428  pm3.22  436  ancoms  439  simpl  443  simpr  447  adantr  451  biimpa  470  biimpar  471  biimpac  472  biimparc  473  pm3.33  568  pm3.34  569  pm3.35  570  pm5.31  571  imp4b  573  imp41  576  imp42  577  imp43  578  imp44  579  imp45  580  imp5g  583  expr  598  impac  604  sylan9  638  sylan9r  639  imdistani  671  jaoian  759  jaodan  760  anabsi5  790  anim12dan  810  pm5.21  831  pm3.43  832  orcanai  879  pm4.82  894  3jcad  1133  3expia  1153  3an1rs  1163  3imp1  1164  3imp2  1166  syl3anl2  1231  3jaoian  1247  3jaodan  1248  mp3anl1  1271  mp3anl2  1272  mp3anl3  1273  alanimi  1562  19.29  1596  nfimdOLD  1809  equs5a  1887  ax12olem3  1929  ax12  1935  dvelimv  1939  ax10  1944  nfeqf  1958  equs4  1959  dvelimh  1964  ax11v2  1992  ax11b  1995  equvin  2001  dfsb2  2055  dvelimdf  2082  sb5rf  2090  dvelimALT  2133  ax12from12o  2156  dvelimf-o  2180  ax11eq  2193  ax11el  2194  ax11indi  2196  ax11indalem  2197  ax11inda2ALT  2198  ax11inda  2200  ax11v2-o  2201  mopick  2266  moexex  2273  exists2  2294  eqrdav  2352  dvelimdc  2510  pm13.18  2589  nelne1  2606  nelne2  2607  ralrimdvv  2709  r19.21bi  2713  r19.26  2747  ralbi  2751  r19.29  2755  vtoclgft  2906  rspcva  2954  rspc2va  2963  elabgt  2983  eqeu  3008  mob2  3017  mob  3019  euind  3024  reu6  3026  reuind  3040  sbctt  3109  rspsbca  3126  csbexg  3147  sbcnestgf  3184  rspcsbela  3196  ssel2  3269  sselda  3274  sstr  3281  nssne1  3328  nssne2  3329  sspsstr  3375  psssstr  3376  neldif  3392  reuss2  3536  reupick  3540  reupick2  3542  reximdva0  3562  ssn0  3584  disjel  3598  ssdisj  3601  disjpss  3602  pssdifn0  3612  uneqdifeq  3639  dedth2h  3705  dedth4h  3707  absneu  3795  uniintsn  3964  dfiun2g  4000  ssofss  4077  opkthg  4132  pw1disj  4168  nncaddccl  4420  nnsucelr  4429  nndisjeq  4430  ncfinlower  4484  nnpw1ex  4485  tfinsuc  4499  tfinltfin  4502  evenoddnnnul  4515  eventfin  4518  oddtfin  4519  nnadjoin  4521  nnpweq  4524  sfindbl  4531  tfinnn  4535  sfinltfin  4536  nulnnn  4557  copsex2t  4609  nbrne1  4657  nbrne2  4658  vtoclr  4817  optocl  4839  funssres  5145  fununi  5161  funimass2  5171  fnun  5190  fco  5232  opelf  5236  f1oun  5305  fun11iun  5306  fv3  5342  fvelima  5370  fvun1  5380  dff3  5421  funfvima2  5461  isotr  5496  isoini  5498  ndmovg  5614  mpteq12f  5656  fvmpti  5700  fvmptf  5723  trtxp  5782  op1st2nd  5791  oqelins4  5795  qrpprod  5837  erth  5969  ectocld  5992  f1oeng  6033  fundmeng  6045  unen  6049  enprmaplem5  6081  nceleq  6150  peano4nc  6151  ce0ncpw1  6186  cecl  6187  sbthlem3  6206  lecponc  6214  leaddc1  6215  leconnnc  6219  dflec3  6222  taddc  6230  ce2le  6234  nclenn  6250  lemuc1  6254  ncslemuc  6256  nmembers1lem2  6270  nnc3n3p1  6279  spacind  6288  nchoicelem3  6292  nchoicelem12  6301  nchoicelem14  6303  nchoicelem15  6304  nchoicelem17  6306  nchoicelem19  6308  frecxp  6315  fnfreclem3  6320  fnfrec  6321