Theorem simp3l 1200

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp13l  1287  simp23l  1293  simp33l  1299  tfisi  7879  fpr3g  8308  tfrlem5  8418  omeulem1  8618  omeulem2  8619  uniinqs  8835  elfiun  9467  tcrank  9921  isfin2-2  10356  konigthlem  10605  gruen  10849  addlid  11441  mulcan  11897  mulcan2  11898  divass  11937  divdir  11944  div11OLD  11948  muldivdir  11957  subdivcomb1  11959  subdivcomb2  11960  divcan5  11966  ltmul1  12114  ltdiv1  12129  ltmuldiv  12138  lediv2  12155  xaddass2  13288  xlt2add  13298  xmulasslem3  13324  xadddi2  13335  expaddz  14143  expmulz  14145  muldivbinom2  14298  resqrtcl  15288  o1add  15646  o1mul  15647  o1sub  15648  dvdsadd2b  16339  dvdsgcd  16577  rpexp12i  16757  pythagtriplem3  16851  pcpremul  16876  pceu  16879  pcqmul  16886  pcqdiv  16890  setsstruct  17209  f1ocpbllem  17570  funcoppc  17925  funcres  17946  catcisolem  18163  1stfcl  18252  2ndfcl  18253  prfcl  18258  evlfcl  18278  curf1cl  18284  curfcl  18288  hofcl  18315  latjlej12  18512  latmlem12  18528  latj4  18546  latj4rot  18547  symgsssg  19499  symgfisg  19500  psgnunilem4  19529  odcong  19581  cmn4  19833  ablsub4  19842  abladdsub4  19843  lsm4  19892  abvdom  20847  abvres  20848  abvtrivd  20849  lspsolvlem  21161  lbsextlem2  21178  lidlsubcl  21251  frlmbas3  21813  matmulcell  22466  marrepeval  22584  ma1repveval  22592  submaeval  22603  mdetunilem3  22635  mdetuni0  22642  mdetmul  22644  minmar1eval  22670  nllyrest  23509  hausflimlem  24002  tsmsxp  24178  psmetlecl  24340  xmetlecl  24371  prdsxmetlem  24393  ngpocelbl  24740  bndth  25003  cph2ass  25260  iscau3  25325  dvres2  25961  coemullem  26303  vieta1  26368  aalioulem4  26391  cxpcn3lem  26804  angcan  26859  dchrvmasumlema  27558  logdivsum  27591  abvcxp  27673  padicabv  27688  nosupbnd1lem4  27770  nosupbnd1lem5  27771  noinfbnd1lem4  27785  cofcut1  27968  cofcut2  27970  divsmulw  28232  precsexlem8  28252  precsexlem9  28253  ax5seglem3  28960  ax5seglem6  28963  axpasch  28970  axeuclid  28992  axcontlem4  28996  axcontlem8  29000  wlkl1loop  29670  trlsonwlkon  29742  pthontrlon  29779  wspthsswwlknon  29950  frgr2wwlkeqm  30359  adjlnop  32114  xreceu  32888  orngmul  33312  rhmdvd  33327  measvunilem  34192  measvunilem0  34193  measres  34202  bnj1128  34982  umgr2cycllem  35124  umgr2cycl  35125  satfv1fvfmla1  35407  cgrcomim  35970  cgrcoml  35977  cgrcomr  35978  cgrdegen  35985  segconeu  35992  btwnintr  36000  btwnexch3  36001  btwnouttr2  36003  btwnouttr  36005  btwnexch  36006  trisegint  36009  lineext  36057  linecgr  36062  lineid  36064  idinside  36065  btwnconn1lem3  36070  btwnconn1lem4  36071  btwnconn1lem7  36074  btwnconn1lem14  36081  btwnconn2  36083  midofsegid  36085  btwnoutside  36106  outsideoftr  36110  lineunray  36128  lineelsb2  36129  cnres2  37749  heibor  37807  lsmcv2  39010  lcvat  39011  lcvexchlem4  39018  lcvexchlem5  39019  lfladd  39047  lflsub  39048  lflmul  39049  lshpkrlem4  39094  latm4  39214  omlmod1i2N  39241  cvlatexch3  39319  cvlsupr7  39329  hlatj4  39355  hlrelat3  39394  cvrval3  39395  atcvrj1  39413  atlelt  39420  2atlt  39421  2atjm  39427  3noncolr2  39431  athgt  39438  3dimlem2  39441  3dimlem4  39446  3dimlem4OLDN  39447  3dim3  39451  1cvratex  39455  ps-1  39459  ps-2  39460  hlatexch3N  39462  llnle  39500  atcvrlln2  39501  atcvrlln  39502  lplni2  39519  lplnle  39522  lplnnle2at  39523  llncvrlpln2  39539  lplnexllnN  39546  2llnmeqat  39553  lvolnle3at  39564  4atlem0ae  39576  lplncvrlvol2  39597  lnjatN  39762  lncvrat  39764  cdlemblem  39775  elpaddri  39784  paddasslem2  39803  paddasslem16  39817  padd4N  39822  hlmod1i  39838  dalawlem2  39854  pclfinN  39882  pexmidlem4N  39955  pl42lem1N  39961  lhp2lt  39983  lhpexle1  39990  lhpexle2lem  39991  lhpj1  40004  lhpmcvr5N  40009  lhp2at0  40014  lhp2atnle  40015  lhp2at0nle  40017  lhple  40024  lhpat  40025  lhpat4N  40026  4atexlempnq  40037  4atexlem7  40057  4atex  40058  ltrn11  40108  ltrnle  40111  ltrnm  40113  ltrnj  40114  ltrncvr  40115  ltrnel  40121  ltrncnvel  40124  ltrncnv  40128  trlval2  40145  trlcnv  40147  trljat1  40148  trljat2  40149  trlat  40151  trl0  40152  trlnidat  40155  trlnid  40161  cdlemc1  40173  cdlemc2  40174  cdlemc5  40177  cdlemd2  40181  cdlemd7  40186  cdlemd8  40187  cdlemd9  40188  cdleme0e  40199  cdleme3g  40216  cdleme3h  40217  cdleme3  40219  cdleme5  40222  cdleme10  40236  cdleme11a  40242  cdleme11c  40243  cdleme11h  40248  cdleme11j  40249  cdleme0nex  40272  cdleme18a  40273  cdleme18b  40274  cdleme22gb  40276  cdleme20zN  40283  cdleme20c  40293  cdleme20k  40301  cdleme21a  40307  cdleme21b  40308  cdleme21c  40309  cdleme21h  40316  cdleme22b  40323  cdleme22d  40325  cdleme22f  40328  cdleme25a  40335  cdleme25c  40337  cdleme25dN  40338  cdleme26ee  40342  cdleme30a  40360  cdlemefr29bpre0N  40388  cdlemefr29clN  40389  cdlemefr32fvaN  40391  cdlemefr32fva1  40392  cdlemefs29bpre0N  40398  cdlemefs29bpre1N  40399  cdlemefs29cpre1N  40400  cdlemefs29clN  40401  cdleme43fsv1snlem  40402  cdlemefs32fvaN  40404  cdlemefs32fva1  40405  cdlemefs31fv1  40406  cdleme36a  40442  cdleme39a  40447  cdleme42a  40453  cdleme42c  40454  cdleme17d3  40478  cdleme48fv  40481  cdleme48bw  40484  cdleme48b  40485  cdlemeg46rgv  40510  cdlemeg46req  40511  cdlemeg46gfv  40512  cdleme48d  40517  cdleme50trn2a  40532  cdleme50trn2  40533  cdleme50ltrn  40539  cdlemf1  40543  cdlemf  40545  trlord  40551  cdlemg2dN  40572  cdlemg2fvlem  40576  cdlemg2l  40585  cdlemg7fvbwN  40589  cdlemg7aN  40607  cdlemg10bALTN  40618  cdlemg10c  40621  cdlemg17a  40643  cdlemg17dALTN  40646  cdlemg31b0a  40677  cdlemg31a  40679  cdlemg31b  40680  cdlemg34  40694  cdlemg36  40696  ltrnco  40701  trlcoabs2N  40704  trlcolem  40708  cdlemg48  40719  tgrpov  40730  tendoco2  40750  tendoplco2  40761  cdlemh1  40797  cdlemi1  40800  cdlemi2  40801  cdlemj3  40805  tendoid0  40807  cdlemk1  40813  cdlemk2  40814  cdlemk4  40816  cdlemk8  40820  cdlemk9  40821  cdlemk9bN  40822  cdlemk10  40825  cdlemk26b-3  40887  cdlemk26-3  40888  cdlemk28-3  40890  cdlemk37  40896  cdlemk39  40898  cdlemkfid1N  40903  cdlemkid1  40904  cdlemky  40908  cdlemkyu  40909  cdlemk19ylem  40912  cdlemk19xlem  40924  cdlemk11t  40928  cdlemk51  40935  cdlemkyyN  40944  cdleml6  40963  cdleml7  40964  cdleml8  40965  cdleml9  40966  erngdvlem4  40973  erngdvlem4-rN  40981  tendospcanN  41005  dia11N  41030  cdlemm10N  41100  dib11N  41142  dicvaddcl  41172  dicvscacl  41173  cdlemn6  41184  dihvalcq2  41229  dihopelvalcpre  41230  dihord6b  41242  dihord5apre  41244  dihmeetlem1N  41272  dihmeetlem2N  41281  dihglbcpreN  41282  dihjatc1  41293  dihmeetlem20N  41308  dih1dimatlem0  41310  dihatlat  41316  dihglblem6  41322  dochexmidlem4  41445  mapdpglem32  41687  mapdh8ad  41761  mapdh9aOLDN  41772  hdmap11lem2  41824  hdmap14lem6  41855  frlmfzowrdb  42490  flt4lem5  42636  mzpsubst  42735  pellex  42822  pellfundex  42873  pellfund14gap  42874  qirropth  42895  rmxypos  42935  congmul  42955  congsub  42958  mzpcong  42960  coprmdvdsb  42973  jm2.15nn0  42991  jm2.16nn0  42992  rpnnen3lem  43019  idomsubgmo  43181  relexp01min  43702  mullimc  45571  islptre  45574  limccog  45575  mullimcf  45578  addlimc  45603  0ellimcdiv  45604  limsupre3lem  45687  stoweidlem57  46012  fourierdlem48  46109  fourierdlem80  46141  fourierdlem113  46174  ovncvrrp  46519  opnvonmbllem2  46588  ovolval5lem3  46609  ovnovollem3  46613  itsclc0lem1  48605  itsclc0lem2  48606  itschlc0yqe  48609  itscnhlc0xyqsol  48614  itschlc0xyqsol1  48615