Theorem simp3l 1202

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 1135	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  1289  simp23l  1295  simp33l  1301  tfisi  7801  fpr3g  8227  tfrlem5  8311  omeulem1  8509  omeulem2  8510  uniinqs  8734  elfiun  9333  tcrank  9796  isfin2-2  10229  konigthlem  10479  gruen  10723  addlid  11316  mulcan  11774  mulcan2  11775  divass  11814  divdir  11821  div11OLD  11825  muldivdir  11834  subdivcomb1  11836  subdivcomb2  11837  divcan5  11843  ltmul1  11991  ltdiv1  12006  ltmuldiv  12015  lediv2  12032  xaddass2  13165  xlt2add  13175  xmulasslem3  13201  xadddi2  13212  expaddz  14029  expmulz  14031  muldivbinom2  14186  resqrtcl  15176  o1add  15537  o1mul  15538  o1sub  15539  dvdsadd2b  16233  dvdsgcd  16471  rpexp12i  16651  pythagtriplem3  16746  pcpremul  16771  pceu  16774  pcqmul  16781  pcqdiv  16785  setsstruct  17103  f1ocpbllem  17445  funcoppc  17799  funcres  17820  catcisolem  18034  1stfcl  18120  2ndfcl  18121  prfcl  18126  evlfcl  18145  curf1cl  18151  curfcl  18155  hofcl  18182  latjlej12  18378  latmlem12  18394  latj4  18412  latj4rot  18413  symgsssg  19396  symgfisg  19397  psgnunilem4  19426  odcong  19478  cmn4  19730  ablsub4  19739  abladdsub4  19740  lsm4  19789  abvdom  20763  abvres  20764  abvtrivd  20765  orngmul  20798  lspsolvlem  21097  lbsextlem2  21114  lidlsubcl  21179  frlmbas3  21731  matmulcell  22389  marrepeval  22507  ma1repveval  22515  submaeval  22526  mdetunilem3  22558  mdetuni0  22565  mdetmul  22567  minmar1eval  22593  nllyrest  23430  hausflimlem  23923  tsmsxp  24099  psmetlecl  24259  xmetlecl  24290  prdsxmetlem  24312  ngpocelbl  24648  bndth  24913  cph2ass  25169  iscau3  25234  dvres2  25869  coemullem  26211  vieta1  26276  aalioulem4  26299  cxpcn3lem  26713  angcan  26768  dchrvmasumlema  27467  logdivsum  27500  abvcxp  27582  padicabv  27597  nosupbnd1lem4  27679  nosupbnd1lem5  27680  noinfbnd1lem4  27694  cofcut1  27916  cofcut2  27918  divmulsw  28189  precsexlem8  28210  precsexlem9  28211  bdayfinbndlem1  28463  ax5seglem3  29004  ax5seglem6  29007  axpasch  29014  axeuclid  29036  axcontlem4  29040  axcontlem8  29044  wlkl1loop  29711  trlsonwlkon  29781  pthontrlon  29820  wspthsswwlknon  29994  frgr2wwlkeqm  30406  adjlnop  32161  xreceu  33003  rhmdvd  33405  measvunilem  34369  measvunilem0  34370  measres  34379  bnj1128  35146  umgr2cycllem  35334  umgr2cycl  35335  satfv1fvfmla1  35617  cgrcomim  36183  cgrcoml  36190  cgrcomr  36191  cgrdegen  36198  segconeu  36205  btwnintr  36213  btwnexch3  36214  btwnouttr2  36216  btwnouttr  36218  btwnexch  36219  trisegint  36222  lineext  36270  linecgr  36275  lineid  36277  idinside  36278  btwnconn1lem3  36283  btwnconn1lem4  36284  btwnconn1lem7  36287  btwnconn1lem14  36294  btwnconn2  36296  midofsegid  36298  btwnoutside  36319  outsideoftr  36323  lineunray  36341  lineelsb2  36342  cnres2  37960  heibor  38018  lsmcv2  39285  lcvat  39286  lcvexchlem4  39293  lcvexchlem5  39294  lfladd  39322  lflsub  39323  lflmul  39324  lshpkrlem4  39369  latm4  39489  omlmod1i2N  39516  cvlatexch3  39594  cvlsupr7  39604  hlatj4  39630  hlrelat3  39668  cvrval3  39669  atcvrj1  39687  atlelt  39694  2atlt  39695  2atjm  39701  3noncolr2  39705  athgt  39712  3dimlem2  39715  3dimlem4  39720  3dimlem4OLDN  39721  3dim3  39725  1cvratex  39729  ps-1  39733  ps-2  39734  hlatexch3N  39736  llnle  39774  atcvrlln2  39775  atcvrlln  39776  lplni2  39793  lplnle  39796  lplnnle2at  39797  llncvrlpln2  39813  lplnexllnN  39820  2llnmeqat  39827  lvolnle3at  39838  4atlem0ae  39850  lplncvrlvol2  39871  lnjatN  40036  lncvrat  40038  cdlemblem  40049  elpaddri  40058  paddasslem2  40077  paddasslem16  40091  padd4N  40096  hlmod1i  40112  dalawlem2  40128  pclfinN  40156  pexmidlem4N  40229  pl42lem1N  40235  lhp2lt  40257  lhpexle1  40264  lhpexle2lem  40265  lhpj1  40278  lhpmcvr5N  40283  lhp2at0  40288  lhp2atnle  40289  lhp2at0nle  40291  lhple  40298  lhpat  40299  lhpat4N  40300  4atexlempnq  40311  4atexlem7  40331  4atex  40332  ltrn11  40382  ltrnle  40385  ltrnm  40387  ltrnj  40388  ltrncvr  40389  ltrnel  40395  ltrncnvel  40398  ltrncnv  40402  trlval2  40419  trlcnv  40421  trljat1  40422  trljat2  40423  trlat  40425  trl0  40426  trlnidat  40429  trlnid  40435  cdlemc1  40447  cdlemc2  40448  cdlemc5  40451  cdlemd2  40455  cdlemd7  40460  cdlemd8  40461  cdlemd9  40462  cdleme0e  40473  cdleme3g  40490  cdleme3h  40491  cdleme3  40493  cdleme5  40496  cdleme10  40510  cdleme11a  40516  cdleme11c  40517  cdleme11h  40522  cdleme11j  40523  cdleme0nex  40546  cdleme18a  40547  cdleme18b  40548  cdleme22gb  40550  cdleme20zN  40557  cdleme20c  40567  cdleme20k  40575  cdleme21a  40581  cdleme21b  40582  cdleme21c  40583  cdleme21h  40590  cdleme22b  40597  cdleme22d  40599  cdleme22f  40602  cdleme25a  40609  cdleme25c  40611  cdleme25dN  40612  cdleme26ee  40616  cdleme30a  40634  cdlemefr29bpre0N  40662  cdlemefr29clN  40663  cdlemefr32fvaN  40665  cdlemefr32fva1  40666  cdlemefs29bpre0N  40672  cdlemefs29bpre1N  40673  cdlemefs29cpre1N  40674  cdlemefs29clN  40675  cdleme43fsv1snlem  40676  cdlemefs32fvaN  40678  cdlemefs32fva1  40679  cdlemefs31fv1  40680  cdleme36a  40716  cdleme39a  40721  cdleme42a  40727  cdleme42c  40728  cdleme17d3  40752  cdleme48fv  40755  cdleme48bw  40758  cdleme48b  40759  cdlemeg46rgv  40784  cdlemeg46req  40785  cdlemeg46gfv  40786  cdleme48d  40791  cdleme50trn2a  40806  cdleme50trn2  40807  cdleme50ltrn  40813  cdlemf1  40817  cdlemf  40819  trlord  40825  cdlemg2dN  40846  cdlemg2fvlem  40850  cdlemg2l  40859  cdlemg7fvbwN  40863  cdlemg7aN  40881  cdlemg10bALTN  40892  cdlemg10c  40895  cdlemg17a  40917  cdlemg17dALTN  40920  cdlemg31b0a  40951  cdlemg31a  40953  cdlemg31b  40954  cdlemg34  40968  cdlemg36  40970  ltrnco  40975  trlcoabs2N  40978  trlcolem  40982  cdlemg48  40993  tgrpov  41004  tendoco2  41024  tendoplco2  41035  cdlemh1  41071  cdlemi1  41074  cdlemi2  41075  cdlemj3  41079  tendoid0  41081  cdlemk1  41087  cdlemk2  41088  cdlemk4  41090  cdlemk8  41094  cdlemk9  41095  cdlemk9bN  41096  cdlemk10  41099  cdlemk26b-3  41161  cdlemk26-3  41162  cdlemk28-3  41164  cdlemk37  41170  cdlemk39  41172  cdlemkfid1N  41177  cdlemkid1  41178  cdlemky  41182  cdlemkyu  41183  cdlemk19ylem  41186  cdlemk19xlem  41198  cdlemk11t  41202  cdlemk51  41209  cdlemkyyN  41218  cdleml6  41237  cdleml7  41238  cdleml8  41239  cdleml9  41240  erngdvlem4  41247  erngdvlem4-rN  41255  tendospcanN  41279  dia11N  41304  cdlemm10N  41374  dib11N  41416  dicvaddcl  41446  dicvscacl  41447  cdlemn6  41458  dihvalcq2  41503  dihopelvalcpre  41504  dihord6b  41516  dihord5apre  41518  dihmeetlem1N  41546  dihmeetlem2N  41555  dihglbcpreN  41556  dihjatc1  41567  dihmeetlem20N  41582  dih1dimatlem0  41584  dihatlat  41590  dihglblem6  41596  dochexmidlem4  41719  mapdpglem32  41961  mapdh8ad  42035  mapdh9aOLDN  42046  hdmap11lem2  42098  hdmap14lem6  42129  frlmfzowrdb  42755  flt4lem5  42889  mzpsubst  42986  pellex  43073  pellfundex  43124  pellfund14gap  43125  qirropth  43146  rmxypos  43185  congmul  43205  congsub  43208  mzpcong  43210  coprmdvdsb  43223  jm2.15nn0  43241  jm2.16nn0  43242  rpnnen3lem  43269  idomsubgmo  43431  relexp01min  43950  mullimc  45858  islptre  45861  limccog  45862  mullimcf  45865  addlimc  45888  0ellimcdiv  45889  limsupre3lem  45972  stoweidlem57  46297  fourierdlem48  46394  fourierdlem80  46426  fourierdlem113  46459  ovncvrrp  46804  opnvonmbllem2  46873  ovolval5lem3  46894  ovnovollem3  46898  grlimedgclnbgr  48237  itsclc0lem1  48998  itsclc0lem2  48999  itschlc0yqe  49002  itscnhlc0xyqsol  49007  itschlc0xyqsol1  49008  swapffunc  49523  fucofunc  49600  fucoppc  49651