Theorem simp3l 1220

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 487	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2ant3 1153	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  simp13l  1307  simp23l  1313  simp33l  1319  tfisi  7856  fpr3g  8283  tfrlem5  8367  omeulem1  8568  omeulem2  8569  uniinqs  8796  elfiun  9391  tcrank  9857  isfin2-2  10304  konigthlem  10554  gruen  10798  addlid  11394  mulcan  11852  mulcan2  11853  divass  11891  divdir  11898  muldivdir  11908  subdivcomb1  11911  subdivcomb2  11912  divcan5  11918  ltmul1  12066  ltdiv1  12080  ltmuldiv  12089  lediv2  12106  xaddass2  13277  xlt2add  13287  xmulasslem3  13313  xadddi2  13324  expaddz  14144  expmulz  14146  muldivbinom2  14301  resqrtcl  15306  o1add  15667  o1mul  15668  o1sub  15669  dvdsadd2b  16365  dvdsgcd  16603  rpexp12i  16784  pythagtriplem3  16879  pcpremul  16904  pceu  16907  pcqmul  16914  pcqdiv  16918  setsstruct  17237  f1ocpbllem  17579  funcoppc  17933  funcres  17954  catcisolem  18168  1stfcl  18254  2ndfcl  18255  prfcl  18260  evlfcl  18279  curf1cl  18285  curfcl  18289  hofcl  18316  latjlej12  18512  latmlem12  18528  latj4  18546  latj4rot  18547  symgsssg  19538  symgfisg  19539  psgnunilem4  19568  odcong  19620  cmn4  19872  ablsub4  19881  abladdsub4  19882  lsm4  19931  abvdom  20914  abvres  20915  abvtrivd  20916  orngmul  20949  lspsolvlem  21247  lbsextlem2  21264  lidlsubcl  21330  frlmbas3  21907  matmulcell  22583  marrepeval  22701  ma1repveval  22709  submaeval  22720  mdetunilem3  22752  mdetuni0  22759  mdetmul  22761  minmar1eval  22787  nllyrest  23624  hausflimlem  24117  tsmsxp  24293  psmetlecl  24453  xmetlecl  24484  prdsxmetlem  24506  ngpocelbl  24842  bndth  25098  cph2ass  25353  iscau3  25418  dvres2  26052  coemullem  26388  vieta1  26454  aalioulem4  26479  cxpcn3lem  26893  angcan  26948  dchrvmasumlema  27645  logdivsum  27678  abvcxp  27760  padicabv  27775  nosupbnd1lem4  27856  nosupbnd1lem5  27857  noinfbnd1lem4  27871  cofcut1  28094  cofcut2  28096  divmulsw  28367  precsexlem8  28388  precsexlem9  28389  bdayfinbndlem1  28641  ax5seglem3  29262  ax5seglem6  29265  axpasch  29272  axeuclid  29294  axcontlem4  29298  axcontlem8  29302  wlkl1loop  29968  trlsonwlkon  30038  pthontrlon  30077  wspthsswwlknon  30251  frgr2wwlkeqm  30663  adjlnop  32419  xreceu  33222  rhmdvd  33625  measvunilem  34583  measvunilem0  34584  measres  34593  bnj1128  35359  umgr2cycllem  35613  umgr2cycl  35614  satfv1fvfmla1  35896  cgrcomim  36462  cgrcoml  36469  cgrcomr  36470  cgrdegen  36477  segconeu  36484  btwnintr  36492  btwnexch3  36493  btwnouttr2  36495  btwnouttr  36497  btwnexch  36498  trisegint  36501  lineext  36549  linecgr  36554  lineid  36556  idinside  36557  btwnconn1lem3  36562  btwnconn1lem4  36563  btwnconn1lem7  36566  btwnconn1lem14  36573  btwnconn2  36575  midofsegid  36577  btwnoutside  36598  outsideoftr  36602  lineunray  36620  lineelsb2  36621  cnres2  38395  heibor  38453  lsmcv2  39784  lcvat  39785  lcvexchlem4  39792  lcvexchlem5  39793  lfladd  39821  lflsub  39822  lflmul  39823  lshpkrlem4  39868  latm4  39988  omlmod1i2N  40015  cvlatexch3  40093  cvlsupr7  40103  hlatj4  40129  hlrelat3  40167  cvrval3  40168  atcvrj1  40186  atlelt  40193  2atlt  40194  2atjm  40200  3noncolr2  40204  athgt  40211  3dimlem2  40214  3dimlem4  40219  3dimlem4OLDN  40220  3dim3  40224  1cvratex  40228  ps-1  40232  ps-2  40233  hlatexch3N  40235  llnle  40273  atcvrlln2  40274  atcvrlln  40275  lplni2  40292  lplnle  40295  lplnnle2at  40296  llncvrlpln2  40312  lplnexllnN  40319  2llnmeqat  40326  lvolnle3at  40337  4atlem0ae  40349  lplncvrlvol2  40370  lnjatN  40535  lncvrat  40537  cdlemblem  40548  elpaddri  40557  paddasslem2  40576  paddasslem16  40590  padd4N  40595  hlmod1i  40611  dalawlem2  40627  pclfinN  40655  pexmidlem4N  40728  pl42lem1N  40734  lhp2lt  40756  lhpexle1  40763  lhpexle2lem  40764  lhpj1  40777  lhpmcvr5N  40782  lhp2at0  40787  lhp2atnle  40788  lhp2at0nle  40790  lhple  40797  lhpat  40798  lhpat4N  40799  4atexlempnq  40810  4atexlem7  40830  4atex  40831  ltrn11  40881  ltrnle  40884  ltrnm  40886  ltrnj  40887  ltrncvr  40888  ltrnel  40894  ltrncnvel  40897  ltrncnv  40901  trlval2  40918  trlcnv  40920  trljat1  40921  trljat2  40922  trlat  40924  trl0  40925  trlnidat  40928  trlnid  40934  cdlemc1  40946  cdlemc2  40947  cdlemc5  40950  cdlemd2  40954  cdlemd7  40959  cdlemd8  40960  cdlemd9  40961  cdleme0e  40972  cdleme3g  40989  cdleme3h  40990  cdleme3  40992  cdleme5  40995  cdleme10  41009  cdleme11a  41015  cdleme11c  41016  cdleme11h  41021  cdleme11j  41022  cdleme0nex  41045  cdleme18a  41046  cdleme18b  41047  cdleme22gb  41049  cdleme20zN  41056  cdleme20c  41066  cdleme20k  41074  cdleme21a  41080  cdleme21b  41081  cdleme21c  41082  cdleme21h  41089  cdleme22b  41096  cdleme22d  41098  cdleme22f  41101  cdleme25a  41108  cdleme25c  41110  cdleme25dN  41111  cdleme26ee  41115  cdleme30a  41133  cdlemefr29bpre0N  41161  cdlemefr29clN  41162  cdlemefr32fvaN  41164  cdlemefr32fva1  41165  cdlemefs29bpre0N  41171  cdlemefs29bpre1N  41172  cdlemefs29cpre1N  41173  cdlemefs29clN  41174  cdleme43fsv1snlem  41175  cdlemefs32fvaN  41177  cdlemefs32fva1  41178  cdlemefs31fv1  41179  cdleme36a  41215  cdleme39a  41220  cdleme42a  41226  cdleme42c  41227  cdleme17d3  41251  cdleme48fv  41254  cdleme48bw  41257  cdleme48b  41258  cdlemeg46rgv  41283  cdlemeg46req  41284  cdlemeg46gfv  41285  cdleme48d  41290  cdleme50trn2a  41305  cdleme50trn2  41306  cdleme50ltrn  41312  cdlemf1  41316  cdlemf  41318  trlord  41324  cdlemg2dN  41345  cdlemg2fvlem  41349  cdlemg2l  41358  cdlemg7fvbwN  41362  cdlemg7aN  41380  cdlemg10bALTN  41391  cdlemg10c  41394  cdlemg17a  41416  cdlemg17dALTN  41419  cdlemg31b0a  41450  cdlemg31a  41452  cdlemg31b  41453  cdlemg34  41467  cdlemg36  41469  ltrnco  41474  trlcoabs2N  41477  trlcolem  41481  cdlemg48  41492  tgrpov  41503  tendoco2  41523  tendoplco2  41534  cdlemh1  41570  cdlemi1  41573  cdlemi2  41574  cdlemj3  41578  tendoid0  41580  cdlemk1  41586  cdlemk2  41587  cdlemk4  41589  cdlemk8  41593  cdlemk9  41594  cdlemk9bN  41595  cdlemk10  41598  cdlemk26b-3  41660  cdlemk26-3  41661  cdlemk28-3  41663  cdlemk37  41669  cdlemk39  41671  cdlemkfid1N  41676  cdlemkid1  41677  cdlemky  41681  cdlemkyu  41682  cdlemk19ylem  41685  cdlemk19xlem  41697  cdlemk11t  41701  cdlemk51  41708  cdlemkyyN  41717  cdleml6  41736  cdleml7  41737  cdleml8  41738  cdleml9  41739  erngdvlem4  41746  erngdvlem4-rN  41754  tendospcanN  41778  dia11N  41803  cdlemm10N  41873  dib11N  41915  dicvaddcl  41945  dicvscacl  41946  cdlemn6  41957  dihvalcq2  42002  dihopelvalcpre  42003  dihord6b  42015  dihord5apre  42017  dihmeetlem1N  42045  dihmeetlem2N  42054  dihglbcpreN  42055  dihjatc1  42066  dihmeetlem20N  42081  dih1dimatlem0  42083  dihatlat  42089  dihglblem6  42095  dochexmidlem4  42218  mapdpglem32  42460  mapdh8ad  42534  mapdh9aOLDN  42545  hdmap11lem2  42597  hdmap14lem6  42628  frlmfzowrdb  43259  flt4lem5  43365  mzpsubst  43462  pellex  43545  pellfundex  43596  pellfund14gap  43597  qirropth  43618  rmxypos  43657  congmul  43677  congsub  43680  mzpcong  43682  coprmdvdsb  43695  jm2.15nn0  43713  jm2.16nn0  43714  rpnnen3lem  43741  idomsubgmo  43903  relexp01min  44422  mullimc  46315  islptre  46318  limccog  46319  mullimcf  46322  addlimc  46345  0ellimcdiv  46346  limsupre3lem  46429  stoweidlem57  46754  fourierdlem48  46851  fourierdlem80  46883  fourierdlem113  46916  ovncvrrp  47261  opnvonmbllem2  47330  ovolval5lem3  47351  ovnovollem3  47355  grlimedgclnbgr  48743  itsclc0lem1  49519  itsclc0lem2  49520  itschlc0yqe  49523  itscnhlc0xyqsol  49528  itschlc0xyqsol1  49529  swapffunc  50043  fucofunc  50120  fucoppc  50171