Theorem simp3l 1089

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

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

Proof of Theorem simp3l

Step	Hyp	Ref	Expression
1		simpl 473	. 2 |- ( ( ch /\ th ) -> ch )
2	1	3ad2ant3 1084	1 |- ( ( ph /\ ps /\ ( ch /\ th ) ) -> ch )

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:  simpl3l  1116  simpr3l  1122  simp13l  1176  simp23l  1182  simp33l  1188  tfisi  7058  tfrlem5  7476  omeulem1  7662  omeulem2  7663  uniinqs  7827  elfiun  8336  tcrank  8747  isfin2-2  9141  konigthlem  9390  gruen  9634  addid2  10219  mulcan  10664  mulcan2  10665  divass  10703  divdir  10710  div11  10713  muldivdir  10720  divcan5  10727  ltmul1  10873  ltdiv1  10887  ltmuldiv  10896  lediv2  10913  xaddass2  12080  xlt2add  12090  xmulasslem3  12116  xadddi2  12127  expaddz  12904  expmulz  12906  muldivbinom2  13047  resqrtcl  13994  o1add  14344  o1mul  14345  o1sub  14346  dvdsadd2b  15028  dvdsgcd  15261  rpexp12i  15434  pythagtriplem3  15523  pcpremul  15548  pceu  15551  pcqmul  15558  pcqdiv  15562  setsstruct  15898  f1ocpbllem  16184  funcoppc  16535  funcres  16556  catcisolem  16756  1stfcl  16837  2ndfcl  16838  prfcl  16843  evlfcl  16862  curf1cl  16868  curfcl  16872  hofcl  16899  latjlej12  17067  latmlem12  17083  latj4  17101  latj4rot  17102  symgsssg  17887  symgfisg  17888  psgnunilem4  17917  odcong  17968  cmn4  18212  ablsub4  18218  abladdsub4  18219  lsm4  18263  abvdom  18838  abvres  18839  abvtrivd  18840  lspsolvlem  19142  lbsextlem2  19159  lidlsubcl  19216  frlmbas3  20115  matmulcell  20251  marrepeval  20369  ma1repveval  20377  submaeval  20388  mdetunilem3  20420  mdetuni0  20427  mdetmul  20429  minmar1eval  20455  nllyrest  21289  hausflimlem  21783  tsmsxp  21958  psmetlecl  22120  xmetlecl  22151  prdsxmetlem  22173  ngpocelbl  22508  bndth  22757  cph2ass  23013  iscau3  23076  dvres2  23676  coemullem  24006  vieta1  24067  aalioulem4  24090  cxpcn3lem  24488  angcan  24532  dchrvmasumlema  25189  logdivsum  25222  abvcxp  25304  padicabv  25319  ax5seglem3  25811  ax5seglem6  25814  axpasch  25821  axeuclid  25843  axcontlem4  25847  axcontlem8  25851  wlkl1loop  26534  trlsonwlkon  26606  pthontrlon  26643  wspthsswwlknon  26817  frgr2wwlkeqm  27195  adjlnop  28945  xreceu  29630  orngmul  29803  rhmdvd  29821  measvunilem  30275  measvunilem0  30276  measres  30285  bnj1128  31058  subdivcomb1  31611  subdivcomb2  31612  nosupbnd1lem4  31857  nosupbnd1lem5  31858  cgrcomim  32096  cgrcoml  32103  cgrcomr  32104  cgrdegen  32111  segconeu  32118  btwnintr  32126  btwnexch3  32127  btwnouttr2  32129  btwnouttr  32131  btwnexch  32132  trisegint  32135  lineext  32183  linecgr  32188  lineid  32190  idinside  32191  btwnconn1lem3  32196  btwnconn1lem4  32197  btwnconn1lem7  32200  btwnconn1lem14  32207  btwnconn2  32209  midofsegid  32211  btwnoutside  32232  outsideoftr  32236  lineunray  32254  lineelsb2  32255  cnres2  33562  heibor  33620  lsmcv2  34316  lcvat  34317  lcvexchlem4  34324  lcvexchlem5  34325  lfladd  34353  lflsub  34354  lflmul  34355  lshpkrlem4  34400  latm4  34520  omlmod1i2N  34547  cvlatexch3  34625  cvlsupr7  34635  hlatj4  34660  hlrelat3  34698  cvrval3  34699  atcvrj1  34717  atlelt  34724  2atlt  34725  2atjm  34731  3noncolr2  34735  athgt  34742  3dimlem2  34745  3dimlem4  34750  3dimlem4OLDN  34751  3dim3  34755  1cvratex  34759  ps-1  34763  ps-2  34764  hlatexch3N  34766  llnle  34804  atcvrlln2  34805  atcvrlln  34806  lplni2  34823  lplnle  34826  lplnnle2at  34827  llncvrlpln2  34843  lplnexllnN  34850  2llnmeqat  34857  lvolnle3at  34868  4atlem0ae  34880  lplncvrlvol2  34901  lnjatN  35066  lncvrat  35068  cdlemblem  35079  elpaddri  35088  paddasslem2  35107  paddasslem16  35121  padd4N  35126  hlmod1i  35142  dalawlem2  35158  pclfinN  35186  pexmidlem4N  35259  pl42lem1N  35265  lhp2lt  35287  lhpexle1  35294  lhpexle2lem  35295  lhpj1  35308  lhpmcvr5N  35313  lhp2at0  35318  lhp2atnle  35319  lhp2at0nle  35321  lhple  35328  lhpat  35329  lhpat4N  35330  4atexlempnq  35341  4atexlem7  35361  4atex  35362  ltrn11  35412  ltrnle  35415  ltrnm  35417  ltrnj  35418  ltrncvr  35419  ltrnel  35425  ltrncnvel  35428  ltrncnv  35432  ltrnmwOLD  35438  trlval2  35450  trlcnv  35452  trljat1  35453  trljat2  35454  trlat  35456  trl0  35457  trlnidat  35460  trlnid  35466  cdlemc1  35478  cdlemc2  35479  cdlemc5  35482  cdlemd2  35486  cdlemd7  35491  cdlemd8  35492  cdlemd9  35493  cdleme0e  35504  cdleme3g  35521  cdleme3h  35522  cdleme3  35524  cdleme5  35527  cdleme10  35541  cdleme11a  35547  cdleme11c  35548  cdleme11h  35553  cdleme11j  35554  cdleme0nex  35577  cdleme18a  35578  cdleme18b  35579  cdleme22gb  35581  cdleme20zN  35588  cdleme20yOLD  35590  cdleme20c  35599  cdleme20k  35607  cdleme21a  35613  cdleme21b  35614  cdleme21c  35615  cdleme21h  35622  cdleme22b  35629  cdleme22d  35631  cdleme22f  35634  cdleme25a  35641  cdleme25c  35643  cdleme25dN  35644  cdleme26ee  35648  cdleme30a  35666  cdlemefr29bpre0N  35694  cdlemefr29clN  35695  cdlemefr32fvaN  35697  cdlemefr32fva1  35698  cdlemefs29bpre0N  35704  cdlemefs29bpre1N  35705  cdlemefs29cpre1N  35706  cdlemefs29clN  35707  cdleme43fsv1snlem  35708  cdlemefs32fvaN  35710  cdlemefs32fva1  35711  cdlemefs31fv1  35712  cdleme36a  35748  cdleme39a  35753  cdleme42a  35759  cdleme42c  35760  cdleme17d3  35784  cdleme48fv  35787  cdleme48bw  35790  cdleme48b  35791  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemeg46gfv  35818  cdleme48d  35823  cdleme50trn2a  35838  cdleme50trn2  35839  cdleme50ltrn  35845  cdlemf1  35849  cdlemf  35851  trlord  35857  cdlemg2dN  35878  cdlemg2fvlem  35882  cdlemg2l  35891  cdlemg7fvbwN  35895  cdlemg7aN  35913  cdlemg10bALTN  35924  cdlemg10c  35927  cdlemg17a  35949  cdlemg17dALTN  35952  cdlemg31b0a  35983  cdlemg31a  35985  cdlemg31b  35986  cdlemg34  36000  cdlemg36  36002  ltrnco  36007  trlcoabs2N  36010  trlcolem  36014  cdlemg48  36025  tgrpov  36036  tendoco2  36056  tendoplco2  36067  cdlemh1  36103  cdlemi1  36106  cdlemi2  36107  cdlemj3  36111  tendoid0  36113  cdlemk1  36119  cdlemk2  36120  cdlemk4  36122  cdlemk8  36126  cdlemk9  36127  cdlemk9bN  36128  cdlemk10  36131  cdlemk26b-3  36193  cdlemk26-3  36194  cdlemk28-3  36196  cdlemk37  36202  cdlemk39  36204  cdlemkfid1N  36209  cdlemkid1  36210  cdlemky  36214  cdlemkyu  36215  cdlemk19ylem  36218  cdlemk19xlem  36230  cdlemk11t  36234  cdlemk51  36241  cdlemkyyN  36250  cdleml6  36269  cdleml7  36270  cdleml8  36271  cdleml9  36272  erngdvlem4  36279  erngdvlem4-rN  36287  tendospcanN  36312  dia11N  36337  cdlemm10N  36407  dib11N  36449  dicvaddcl  36479  dicvscacl  36480  cdlemn6  36491  dihvalcq2  36536  dihopelvalcpre  36537  dihord6b  36549  dihord5apre  36551  dihmeetlem1N  36579  dihmeetlem2N  36588  dihglbcpreN  36589  dihjatc1  36600  dihmeetlem20N  36615  dih1dimatlem0  36617  dihatlat  36623  dihglblem6  36629  dochexmidlem4  36752  mapdpglem32  36994  mapdh8ad  37068  mapdh9aOLDN  37080  hdmap11lem2  37134  hdmap14lem6  37165  mzpsubst  37311  pellex  37399  pellfundex  37450  pellfund14gap  37451  qirropth  37473  rmxypos  37514  congmul  37534  congsub  37537  mzpcong  37539  coprmdvdsb  37552  jm2.15nn0  37570  jm2.16nn0  37571  rpnnen3lem  37598  idomsubgmo  37776  relexp01min  38005  mullimc  39848  islptre  39851  limccog  39852  mullimcf  39855  addlimc  39880  0ellimcdiv  39881  limsupre3lem  39964  stoweidlem57  40274  fourierdlem48  40371  fourierdlem80  40403  fourierdlem113  40436  ovncvrrp  40778  opnvonmbllem2  40847  ovolval5lem3  40868  ovnovollem3  40872