Theorem simp3l 1214

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

Assertion

Ref	Expression
simp3l	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

Proof of Theorem simp3l

Step	Hyp	Ref	Expression
1		simpl 486	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2ant3 1147	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  simp13l  1301  simp23l  1307  simp33l  1313  tfisi  7835  fpr3g  8261  tfrlem5  8345  omeulem1  8546  omeulem2  8547  uniinqs  8774  elfiun  9373  tcrank  9839  isfin2-2  10273  konigthlem  10523  gruen  10767  addlid  11363  mulcan  11821  mulcan2  11822  divass  11860  divdir  11867  div11OLD  11871  muldivdir  11880  subdivcomb1  11883  subdivcomb2  11884  divcan5  11890  ltmul1  12038  ltdiv1  12053  ltmuldiv  12062  lediv2  12079  xaddass2  13250  xlt2add  13260  xmulasslem3  13286  xadddi2  13297  expaddz  14116  expmulz  14118  muldivbinom2  14273  resqrtcl  15263  o1add  15624  o1mul  15625  o1sub  15626  dvdsadd2b  16323  dvdsgcd  16561  rpexp12i  16742  pythagtriplem3  16837  pcpremul  16862  pceu  16865  pcqmul  16872  pcqdiv  16876  setsstruct  17195  f1ocpbllem  17537  funcoppc  17891  funcres  17912  catcisolem  18126  1stfcl  18212  2ndfcl  18213  prfcl  18218  evlfcl  18237  curf1cl  18243  curfcl  18247  hofcl  18274  latjlej12  18470  latmlem12  18486  latj4  18504  latj4rot  18505  symgsssg  19490  symgfisg  19491  psgnunilem4  19520  odcong  19572  cmn4  19824  ablsub4  19833  abladdsub4  19834  lsm4  19883  abvdom  20859  abvres  20860  abvtrivd  20861  orngmul  20894  lspsolvlem  21192  lbsextlem2  21209  lidlsubcl  21274  frlmbas3  21808  matmulcell  22485  marrepeval  22603  ma1repveval  22611  submaeval  22622  mdetunilem3  22654  mdetuni0  22661  mdetmul  22663  minmar1eval  22689  nllyrest  23526  hausflimlem  24019  tsmsxp  24195  psmetlecl  24355  xmetlecl  24386  prdsxmetlem  24408  ngpocelbl  24744  bndth  25000  cph2ass  25255  iscau3  25320  dvres2  25954  coemullem  26290  vieta1  26353  aalioulem4  26376  cxpcn3lem  26789  angcan  26844  dchrvmasumlema  27541  logdivsum  27574  abvcxp  27656  padicabv  27671  nosupbnd1lem4  27752  nosupbnd1lem5  27753  noinfbnd1lem4  27767  cofcut1  27990  cofcut2  27992  divmulsw  28263  precsexlem8  28284  precsexlem9  28285  bdayfinbndlem1  28537  ax5seglem3  29078  ax5seglem6  29081  axpasch  29088  axeuclid  29110  axcontlem4  29114  axcontlem8  29118  wlkl1loop  29784  trlsonwlkon  29854  pthontrlon  29893  wspthsswwlknon  30067  frgr2wwlkeqm  30479  adjlnop  32235  xreceu  33060  rhmdvd  33471  measvunilem  34470  measvunilem0  34471  measres  34480  bnj1128  35249  umgr2cycllem  35454  umgr2cycl  35455  satfv1fvfmla1  35737  cgrcomim  36303  cgrcoml  36310  cgrcomr  36311  cgrdegen  36318  segconeu  36325  btwnintr  36333  btwnexch3  36334  btwnouttr2  36336  btwnouttr  36338  btwnexch  36339  trisegint  36342  lineext  36390  linecgr  36395  lineid  36397  idinside  36398  btwnconn1lem3  36403  btwnconn1lem4  36404  btwnconn1lem7  36407  btwnconn1lem14  36414  btwnconn2  36416  midofsegid  36418  btwnoutside  36439  outsideoftr  36443  lineunray  36461  lineelsb2  36462  cnres2  38226  heibor  38284  lsmcv2  39617  lcvat  39618  lcvexchlem4  39625  lcvexchlem5  39626  lfladd  39654  lflsub  39655  lflmul  39656  lshpkrlem4  39701  latm4  39821  omlmod1i2N  39848  cvlatexch3  39926  cvlsupr7  39936  hlatj4  39962  hlrelat3  40000  cvrval3  40001  atcvrj1  40019  atlelt  40026  2atlt  40027  2atjm  40033  3noncolr2  40037  athgt  40044  3dimlem2  40047  3dimlem4  40052  3dimlem4OLDN  40053  3dim3  40057  1cvratex  40061  ps-1  40065  ps-2  40066  hlatexch3N  40068  llnle  40106  atcvrlln2  40107  atcvrlln  40108  lplni2  40125  lplnle  40128  lplnnle2at  40129  llncvrlpln2  40145  lplnexllnN  40152  2llnmeqat  40159  lvolnle3at  40170  4atlem0ae  40182  lplncvrlvol2  40203  lnjatN  40368  lncvrat  40370  cdlemblem  40381  elpaddri  40390  paddasslem2  40409  paddasslem16  40423  padd4N  40428  hlmod1i  40444  dalawlem2  40460  pclfinN  40488  pexmidlem4N  40561  pl42lem1N  40567  lhp2lt  40589  lhpexle1  40596  lhpexle2lem  40597  lhpj1  40610  lhpmcvr5N  40615  lhp2at0  40620  lhp2atnle  40621  lhp2at0nle  40623  lhple  40630  lhpat  40631  lhpat4N  40632  4atexlempnq  40643  4atexlem7  40663  4atex  40664  ltrn11  40714  ltrnle  40717  ltrnm  40719  ltrnj  40720  ltrncvr  40721  ltrnel  40727  ltrncnvel  40730  ltrncnv  40734  trlval2  40751  trlcnv  40753  trljat1  40754  trljat2  40755  trlat  40757  trl0  40758  trlnidat  40761  trlnid  40767  cdlemc1  40779  cdlemc2  40780  cdlemc5  40783  cdlemd2  40787  cdlemd7  40792  cdlemd8  40793  cdlemd9  40794  cdleme0e  40805  cdleme3g  40822  cdleme3h  40823  cdleme3  40825  cdleme5  40828  cdleme10  40842  cdleme11a  40848  cdleme11c  40849  cdleme11h  40854  cdleme11j  40855  cdleme0nex  40878  cdleme18a  40879  cdleme18b  40880  cdleme22gb  40882  cdleme20zN  40889  cdleme20c  40899  cdleme20k  40907  cdleme21a  40913  cdleme21b  40914  cdleme21c  40915  cdleme21h  40922  cdleme22b  40929  cdleme22d  40931  cdleme22f  40934  cdleme25a  40941  cdleme25c  40943  cdleme25dN  40944  cdleme26ee  40948  cdleme30a  40966  cdlemefr29bpre0N  40994  cdlemefr29clN  40995  cdlemefr32fvaN  40997  cdlemefr32fva1  40998  cdlemefs29bpre0N  41004  cdlemefs29bpre1N  41005  cdlemefs29cpre1N  41006  cdlemefs29clN  41007  cdleme43fsv1snlem  41008  cdlemefs32fvaN  41010  cdlemefs32fva1  41011  cdlemefs31fv1  41012  cdleme36a  41048  cdleme39a  41053  cdleme42a  41059  cdleme42c  41060  cdleme17d3  41084  cdleme48fv  41087  cdleme48bw  41090  cdleme48b  41091  cdlemeg46rgv  41116  cdlemeg46req  41117  cdlemeg46gfv  41118  cdleme48d  41123  cdleme50trn2a  41138  cdleme50trn2  41139  cdleme50ltrn  41145  cdlemf1  41149  cdlemf  41151  trlord  41157  cdlemg2dN  41178  cdlemg2fvlem  41182  cdlemg2l  41191  cdlemg7fvbwN  41195  cdlemg7aN  41213  cdlemg10bALTN  41224  cdlemg10c  41227  cdlemg17a  41249  cdlemg17dALTN  41252  cdlemg31b0a  41283  cdlemg31a  41285  cdlemg31b  41286  cdlemg34  41300  cdlemg36  41302  ltrnco  41307  trlcoabs2N  41310  trlcolem  41314  cdlemg48  41325  tgrpov  41336  tendoco2  41356  tendoplco2  41367  cdlemh1  41403  cdlemi1  41406  cdlemi2  41407  cdlemj3  41411  tendoid0  41413  cdlemk1  41419  cdlemk2  41420  cdlemk4  41422  cdlemk8  41426  cdlemk9  41427  cdlemk9bN  41428  cdlemk10  41431  cdlemk26b-3  41493  cdlemk26-3  41494  cdlemk28-3  41496  cdlemk37  41502  cdlemk39  41504  cdlemkfid1N  41509  cdlemkid1  41510  cdlemky  41514  cdlemkyu  41515  cdlemk19ylem  41518  cdlemk19xlem  41530  cdlemk11t  41534  cdlemk51  41541  cdlemkyyN  41550  cdleml6  41569  cdleml7  41570  cdleml8  41571  cdleml9  41572  erngdvlem4  41579  erngdvlem4-rN  41587  tendospcanN  41611  dia11N  41636  cdlemm10N  41706  dib11N  41748  dicvaddcl  41778  dicvscacl  41779  cdlemn6  41790  dihvalcq2  41835  dihopelvalcpre  41836  dihord6b  41848  dihord5apre  41850  dihmeetlem1N  41878  dihmeetlem2N  41887  dihglbcpreN  41888  dihjatc1  41899  dihmeetlem20N  41914  dih1dimatlem0  41916  dihatlat  41922  dihglblem6  41928  dochexmidlem4  42051  mapdpglem32  42293  mapdh8ad  42367  mapdh9aOLDN  42378  hdmap11lem2  42430  hdmap14lem6  42461  frlmfzowrdb  43090  flt4lem5  43196  mzpsubst  43293  pellex  43376  pellfundex  43427  pellfund14gap  43428  qirropth  43449  rmxypos  43488  congmul  43508  congsub  43511  mzpcong  43513  coprmdvdsb  43526  jm2.15nn0  43544  jm2.16nn0  43545  rpnnen3lem  43572  idomsubgmo  43734  relexp01min  44253  mullimc  46156  islptre  46159  limccog  46160  mullimcf  46163  addlimc  46186  0ellimcdiv  46187  limsupre3lem  46270  stoweidlem57  46595  fourierdlem48  46692  fourierdlem80  46724  fourierdlem113  46757  ovncvrrp  47102  opnvonmbllem2  47171  ovolval5lem3  47192  ovnovollem3  47196  grlimedgclnbgr  48581  itsclc0lem1  49342  itsclc0lem2  49343  itschlc0yqe  49346  itscnhlc0xyqsol  49351  itschlc0xyqsol1  49352  swapffunc  49867  fucofunc  49944  fucoppc  49995