Theorem impd 447

Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)

Hypothesis

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

Assertion

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

Proof of Theorem impd

Step	Hyp	Ref	Expression
1		impd.1	. . . 4 |- ( ph -> ( ps -> ( ch -> th ) ) )
2	1	com3l 89	. . 3 |- ( ps -> ( ch -> ( ph -> th ) ) )
3	2	imp 445	. 2 |- ( ( ps /\ ch ) -> ( ph -> th ) )
4	3	com12 32	1 |- ( ph -> ( ( ps /\ ch ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  imp32  449  pm3.31  461  syland  498  imp4b  613  imp4c  617  imp4d  618  imp5d  625  expimpd  629  expl  648  3expib  1268  ax13lem1  2248  equs5  2351  rsp2  2936  moi  3389  reu6  3395  sbciegft  3466  elpwunsn  4224  prel12  4383  opthpr  4384  3elpr2eq  4435  invdisj  4638  reusv1OLD  4867  ralxfrd  4879  ralxfrd2  4884  sotr2  5064  wefrc  5108  relop  5272  elres  5435  iss  5447  tz7.7  5749  ordtr2  5768  funssres  5930  fv3  6206  funopsn  6413  fmptsnd  6435  tpres  6466  funfvima  6492  isomin  6587  sorpsscmpl  6948  peano5  7089  f1oweALT  7152  poxp  7289  soxp  7290  wfr3g  7413  tfr3  7495  tz7.48-1  7538  omordi  7646  odi  7659  omass  7660  oen0  7666  nndi  7703  nnmass  7704  nnmordi  7711  nnmord  7712  eroveu  7842  findcard3  8203  fiint  8237  suplub  8366  hartogs  8449  card2on  8459  unxpwdom2  8493  inf3lem2  8526  epfrs  8607  tcel  8621  dfac2  8953  cfcoflem  9094  infpssr  9130  isf32lem9  9183  axdc3lem4  9275  axcclem  9279  zorn2lem7  9324  ttukeylem6  9336  brdom6disj  9354  ondomon  9385  inar1  9597  gruen  9634  indpi  9729  nqereu  9751  genpn0  9825  distrlem1pr  9847  distrlem5pr  9849  ltexprlem1  9858  reclem4pr  9872  addsrmo  9894  mulsrmo  9895  supsrlem  9932  lelttr  10128  ltletr  10129  ltlen  10138  mulgt1  10882  fzind  11475  eqreznegel  11774  xrlelttr  11987  xrltletr  11988  xnn0xaddcl  12066  fzen  12358  elfzodifsumelfzo  12533  bernneq  12990  fundmge2nop0  13274  swrdswrdlem  13459  wrd2ind  13477  reuccats1lem  13479  swrdccatin1  13483  repsdf2  13525  limsupbnd2  14214  rlimuni  14281  mulcn2  14326  rlimno1  14384  prodmolem2  14665  ndvdssub  15133  lcmfunsnlem1  15350  lcmfunsnlem2  15353  coprmdvds  15366  coprmdvdsOLD  15367  coprmdvds2  15368  divgcdcoprm0  15379  maxprmfct  15421  pceu  15551  dvdsprmpweqnn  15589  oddprmdvds  15607  infpnlem1  15614  prmgaplem6  15760  imasaddfnlem  16188  initoeu1  16661  termoeu1  16668  plelttr  16972  gsumval2a  17279  symgfix2  17836  gsmsymgrfixlem1  17847  psgnunilem4  17917  lsmmod  18088  lsmdisj2  18095  efgrelexlemb  18163  pgpfac1lem5  18478  lindfrn  20160  mat1dimcrng  20283  dmatelnd  20302  mdetunilem7  20424  cpmatacl  20521  cpmatmcllem  20523  chfacfisf  20659  chfacfisfcpmat  20660  lmss  21102  lmcnp  21108  hausnei2  21157  isnrm2  21162  isnrm3  21163  cmpsublem  21202  2ndcdisj  21259  1stccnp  21265  txcnpi  21411  txlm  21451  tx1stc  21453  fgss2  21678  fgfil  21679  fgcl  21682  ufileu  21723  rnelfm  21757  fmfnfmlem2  21759  fmfnfmlem4  21761  fmfnfm  21762  ufilcmp  21836  cnpfcf  21845  alexsubALTlem2  21852  alexsubALTlem4  21854  alexsubALT  21855  tmdgsum2  21900  tsmsxp  21958  prdsxmslem2  22334  ivthlem2  23221  ivthlem3  23222  ovolicc2  23290  volfiniun  23315  dyadmax  23366  ellimc3  23643  dvlip2  23758  dvne0  23774  zabsle1  25021  2lgslem3  25129  axcontlem4  25847  umgrislfupgrlem  26017  uhgr2edg  26100  ushgredgedg  26121  ushgredgedgloop  26123  nb3grprlem1  26282  rusgr1vtx  26484  wlkv0  26547  wlkonl1iedg  26561  uhgrwkspthlem2  26650  usgr2wlkneq  26652  usgr2trlncl  26656  uspgrn2crct  26700  wspthsnonn0vne  26813  wwlks2onv  26847  umgrwwlks2on  26850  elwspths2on  26853  erclwwlkstr  26936  erclwwlksntr  26948  frgrnbnb  27157  frgr2wwlk1  27193  frrusgrord  27205  numclwwlkovf2exlem2  27212  frgrregord013  27253  isch3  28098  ocin  28155  shmodsi  28248  spansneleq  28429  stj  29094  atom1d  29212  atcvat2i  29246  chirredlem1  29249  chirredi  29253  mdsymlem3  29264  mdsymlem6  29267  bnj849  30995  pconnconn  31213  cvmsss2  31256  cvmliftlem7  31273  mclsind  31467  dfpo2  31645  dfon2lem9  31696  dfon2  31697  frr3g  31779  frrlem11  31792  scutun12  31917  cgrextend  32115  btwntriv2  32119  btwncomim  32120  btwnexch3  32127  funtransport  32138  ifscgr  32151  colinearxfr  32182  lineext  32183  fscgr  32187  outsideoftr  32236  trer  32310  finminlem  32312  fnessref  32352  fgmin  32365  bj-andnotim  32573  bj-alanim  32596  bj-0int  33055  relowlssretop  33211  finxpsuclem  33234  wl-ax13lem1  33287  poimirlem29  33438  itg2addnclem3  33463  itg2addnc  33464  areacirc  33505  ismtybndlem  33605  heibor1lem  33608  iss2  34112  prtlem17  34161  riotasvd  34242  lshpsmreu  34396  atnle  34604  cvratlem  34707  cvrat2  34715  3dim1  34753  2llnjN  34853  2lplnj  34906  linepsubN  35038  pmapsub  35054  paddasslem14  35119  pclfinN  35186  ispsubcl2N  35233  pclfinclN  35236  ldilval  35399  trlord  35857  cdlemk36  36201  dihlsscpre  36523  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  pellexlem5  37397  pellex  37399  pell1234qrmulcl  37419  pellfundex  37450  relexpmulnn  38001  clsk1indlem3  38341  19.41rg  38766  iunconnlem2  39171  nltle2tri  41323  iccpartnel  41374  fmtnofac2lem  41480  sfprmdvdsmersenne  41520  lighneallem3  41524  lighneallem4  41527  bgoldbtbnd  41697  upgrwlkupwlk  41721  nzerooringczr  42072  ldepspr  42262  aacllem  42547