Theorem 3expia 1267

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

Ref	Expression
3exp.1	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

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

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3exp 1264	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 445	1 |- ( ( ph /\ ps ) -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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  df-3an 1039

This theorem is referenced by:  mp3an3  1413  3gencl  3237  moi  3389  disji  4637  disjord  4641  3optocl  5197  sossfld  5580  f1oresrab  6395  soisores  6577  isomin  6587  isofrlem  6590  ovmpt2s  6784  ov2gf  6785  ndmovord  6824  nnsuc  7082  poxp  7289  brtpos  7361  dfsmo2  7444  smoiun  7458  smoord  7462  smogt  7464  omeulem1  7662  omeu  7665  oewordi  7671  uniinqs  7827  mapvalg  7867  pmvalg  7868  elmapg  7870  xpdom3  8058  mapdom3  8132  php3  8146  unxpdomlem3  8166  isinf  8173  findcard2  8200  isfinite2  8218  ordiso  8421  cnfcom3clem  8602  r111  8638  tskwe  8776  pr2ne  8828  infxpenlem  8836  dfac8alem  8852  infdif  9031  infdif2  9032  cff1  9080  coflim  9083  cfslbn  9089  cfslb2n  9090  cofsmo  9091  cfsmolem  9092  cfcoflem  9094  fin23lem27  9150  isf32lem9  9183  isf34lem6  9202  axcc2lem  9258  domtriomlem  9264  axdc4lem  9277  zorn2lem2  9319  axdclem2  9342  konigthlem  9390  gchen1  9447  gchen2  9448  gchpwdom  9492  gchaleph  9493  winainflem  9515  tskcard  9603  gruiun  9621  gruen  9634  intgru  9636  grudomon  9639  grur1a  9641  grutsk1  9643  nqereu  9751  nqereq  9757  ltsonq  9791  prlem934  9855  reclem3pr  9871  1re  10039  axsup  10113  addid2  10219  recex  10659  lemul1a  10877  lt2msq  10908  fimaxre2  10969  zdiv  11447  zextlt  11451  prime  11458  uzind2  11470  fzind  11475  lbzbi  11776  qbtwnxr  12031  qextltlem  12033  xralrple  12036  xltneg  12048  xlt2add  12090  supxrgtmnf  12159  ixxub  12196  ixxlb  12197  ioo0  12200  ico0  12221  ioc0  12222  icc0  12223  iocssre  12253  icossre  12254  iccssre  12255  fzen  12358  expclzlem  12884  expaddz  12904  expmulz  12906  hashgadd  13166  elovmpt2wrd  13347  ccatopth2  13471  cshf1  13556  shftuz  13809  cau3lem  14094  caubnd  14098  climuni  14283  lo1resb  14295  o1resb  14297  o1of2  14343  o1add  14344  o1mul  14345  o1sub  14346  ntrivcvgmul  14634  eflt  14847  moddvds  14991  dvdscmulr  15010  dvdsmulcr  15011  dvdsle  15032  divalglem8  15123  divalgb  15127  ndvdssub  15133  bitsfzo  15157  gcdcllem1  15221  gcdcllem3  15223  dvdsgcd  15261  lcmgcdlem  15319  lcmfeq0b  15343  qredeu  15372  isprm3  15396  prmdvdsexpr  15429  prmexpb  15430  eulerthlem2  15487  fermltl  15489  coprimeprodsq  15513  pythagtrip  15539  pcprendvds  15545  pcpremul  15548  pcdvdsb  15573  pc2dvds  15583  4sqlem12  15660  4sqlem18  15666  vdwlem10  15694  cshwshashlem3  15804  xpslem  16233  ismred  16262  mrieqv2d  16299  iscatd  16334  isfuncd  16525  fthestrcsetc  16790  fthsetcestrc  16805  poslubd  17148  dirtr  17236  mulgaddcom  17564  ghmrn  17673  pmtrprfv3  17874  mndodcongi  17962  oddvdsnn0  17963  oddvds  17966  odcl2  17982  odhash3  17991  gexdvds  17999  pgpfi  18020  lsmss1b  18080  lsmss2b  18082  efgsrel  18147  efgred  18161  cntzcmn  18245  cyggenod  18286  lt6abl  18296  gsumcom2  18374  pgpfac1lem2  18474  pgpfac1lem3  18476  dvdsunit  18663  unitmulclb  18665  irredrmul  18707  isabvd  18820  lmodvsdi  18886  lss0cl  18947  islbs3  19155  lbsextlem2  19159  mvrf1  19425  coe1fzgsumd  19672  gsummoncoe1  19674  evl1gsumd  19721  xrsdsreclblem  19792  scmataddcl  20322  scmatsubcl  20323  mdetunilem9  20426  mdetuni0  20427  mdetmul  20429  m2cpmrngiso  20563  pm2mpf1  20604  opnnei  20924  neindisj2  20927  cncls2  21077  cncls  21078  cnntr  21079  cnpresti  21092  cnprest  21093  lmcnp  21108  isreg2  21181  ordthauslem  21187  unconn  21232  2ndc1stc  21254  kgen2ss  21358  ptclsg  21418  cnmptcom  21481  kqfvima  21533  hmeof1o  21567  fbncp  21643  fbfinnfr  21645  trfbas2  21647  isufil2  21712  ufprim  21713  trufil  21714  filufint  21724  hausflim  21785  flimrest  21787  flimcls  21789  cnpfcf  21845  alexsubALT  21855  tmdgsum  21899  opnsubg  21911  cldsubg  21914  qustgpopn  21923  tsmsxp  21958  blpnf  22202  blssps  22229  blss  22230  blssec  22240  neibl  22306  prdsxmslem2  22334  xrsmopn  22615  metnrm  22665  climcncf  22703  iccpnfhmeo  22744  xrhmeo  22745  bndth  22757  cphsqrtcl3  22987  iscau2  23075  iscmet3lem2  23090  bcthlem5  23125  bcth3  23128  ishl2  23166  ivthlem1  23220  cmmbl  23302  iundisj2  23317  voliunlem2  23319  mbfaddlem  23427  itg2itg1  23503  itg2seq  23509  itg2mulclem  23513  cnplimc  23651  dvres2  23676  deg1nn0clb  23850  deg1lt0  23851  deg1ge  23858  plypf1  23968  plyadd  23973  plymul  23974  coeeu  23981  dgrub2  23991  coeidlem  23993  coeid3  23996  coemullem  24006  coe11  24009  coemulhi  24010  coemulc  24011  dgreq0  24021  dgrlt  24022  dgradd2  24024  vieta1lem2  24066  tanord1  24283  tanord  24284  logccne0  24325  cxpeq0  24424  cxpmul2z  24437  cxpcn3lem  24488  relogbzcl  24512  angpieqvd  24558  o1cxp  24701  scvxcvx  24712  chtublem  24936  bposlem3  25011  lgsqr  25076  dchrisumlema  25177  dchrisumlem2  25179  ostth2lem3  25324  iscgrglt  25409  tghilberti2  25533  inagswap  25730  f1otrg  25751  brbtwn2  25785  axpasch  25821  axcontlem4  25847  axcontlem5  25848  upgredg2vtx  26036  usgredg2vtxeuALT  26114  sizusglecusg  26359  upgredginwlk  26532  frgrwopreg1  27182  frgrwopreg2  27183  frgrregorufrg  27190  lpni  27332  ipasslem5  27690  htthlem  27774  omlsii  28262  spansni  28416  spansneleq  28429  elspansn4  28432  sumspansn  28508  homco1  28660  homulass  28661  mdsl0  29169  ssdmd1  29172  ssdmd2  29173  cvdmd  29196  chirredlem2  29250  atdmd  29257  atmd2  29259  disjif  29391  iundisj2f  29403  isoun  29479  padct  29497  iocinioc2  29541  iundisj2fi  29556  archiabllem1a  29745  archiabllem2a  29748  slmdvsdi  29768  ordtconnlem1  29970  indpi1  30082  measinblem  30283  measres  30285  measdivcstOLD  30287  mbfmco2  30327  orvclteinc  30537  sgn3da  30603  sgnnbi  30607  sgnpbi  30608  bnj605  30977  bnj607  30986  bnj964  31013  bnj1033  31037  bnj1128  31058  bnj1137  31063  bnj1136  31065  bnj1413  31103  bnj60  31130  cvmlift2lem10  31294  msubvrs  31457  wsuclem  31773  wsuclemOLD  31774  nosepon  31818  noextenddif  31821  nolesgn2o  31824  nosepne  31831  nodense  31842  dfrdg4  32058  brcolinear2  32165  brsegle2  32216  nn0prpw  32318  ntruni  32322  clsint2  32324  fnessref  32352  fnemeet2  32362  fnejoin2  32364  limsucncmpi  32444  ee7.2aOLD  32460  dissneqlem  33187  isbasisrelowllem1  33203  isbasisrelowllem2  33204  icoreclin  33205  poimirlem9  33418  poimirlem30  33439  poimirlem32  33441  areacirc  33505  filbcmb  33535  mettrifi  33553  heiborlem8  33617  heiborlem10  33619  heibor  33620  riscer  33787  igenval2  33865  lshpcmp  34275  eqlkr  34386  lkrlsp2  34390  lkrshp  34392  cvrnbtwn2  34562  cvlexch3  34619  cvlexch4N  34620  cvlatexchb1  34621  cvlsupr3  34631  exatleN  34690  cvratlem  34707  atcvrj2b  34718  cvrat3  34728  cvrat4  34729  athgt  34742  ps-1  34763  ps-2  34764  3atlem5  34773  3at  34776  llnneat  34800  llnmlplnN  34825  lplnneat  34831  lplnnelln  34832  islpln2a  34834  lplnriaN  34836  lplnribN  34837  lplnexllnN  34850  2llnjaN  34852  lvolnle3at  34868  lvolneatN  34874  lvolnelln  34875  lvolnelpln  34876  islvol2aN  34878  dalem62  35020  pmapglb2N  35057  pmapglb2xN  35058  lncmp  35069  paddasslem14  35119  paddasslem15  35120  pmod2iN  35135  hlmod1i  35142  pclfinclN  35236  osumcllem8N  35249  pexmidlem4N  35259  pl42lem1N  35265  pl42lem4N  35268  lhpexle1  35294  lhpexle2lem  35295  lhpmcvr5N  35313  lhpmcvr6N  35314  ltrneq  35435  trlnidatb  35464  cdleme0ex2N  35511  cdleme27a  35655  cdleme17d3  35784  cdlemeg46gfre  35820  cdleme48gfv1  35824  cdlemeg49lebilem  35827  cdlemf2  35850  cdlemf  35851  cdlemfnid  35852  trlord  35857  cdlemg31c  35987  cdlemg35  36001  trlcone  36016  tendoeq2  36062  cdlemj3  36111  cdlemk26b-3  36193  cdlemk33N  36197  cdleml3N  36266  cdlemn  36501  dih1dimb2  36530  dihord5apre  36551  dihmeetlem1N  36579  dihglblem5apreN  36580  dihglblem2N  36583  dihglblem3N  36584  dihmeetlem13N  36608  dihmeetlem15N  36610  dihatexv  36627  hdmap14lem12  37171  oddcomabszz  37509  jm2.19lem4  37559  fiuneneq  37775  idomsubgmo  37776  pwinfi3  37868  gneispa  38428  binomcxplemnn0  38548  addrcom  38679  int3  38837  suctrALT  39061  suctrALTcf  39158  suctrALT3  39160  chordthmALT  39169  iunconnlem2  39171  stoweidlem26  40243  stoweidlem34  40251  issald  40551  goldbachth  41459  nnsgrp  41817  ply1mulgsumlem1  42174