Theorem simp3l 1198

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 1132	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

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

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

This theorem is referenced by:  simp13l  1285  simp23l  1291  simp33l  1297  tfisi  7553  tfrlem5  7999  omeulem1  8191  omeulem2  8192  uniinqs  8360  elfiun  8878  tcrank  9297  isfin2-2  9730  konigthlem  9979  gruen  10223  addid2  10812  mulcan  11266  mulcan2  11267  divass  11305  divdir  11312  div11  11315  muldivdir  11322  subdivcomb1  11324  subdivcomb2  11325  divcan5  11331  ltmul1  11479  ltdiv1  11493  ltmuldiv  11502  lediv2  11519  xaddass2  12631  xlt2add  12641  xmulasslem3  12667  xadddi2  12678  expaddz  13469  expmulz  13471  muldivbinom2  13619  resqrtcl  14605  o1add  14962  o1mul  14963  o1sub  14964  dvdsadd2b  15648  dvdsgcd  15882  rpexp12i  16056  pythagtriplem3  16145  pcpremul  16170  pceu  16173  pcqmul  16180  pcqdiv  16184  setsstruct  16515  f1ocpbllem  16789  funcoppc  17137  funcres  17158  catcisolem  17358  1stfcl  17439  2ndfcl  17440  prfcl  17445  evlfcl  17464  curf1cl  17470  curfcl  17474  hofcl  17501  latjlej12  17669  latmlem12  17685  latj4  17703  latj4rot  17704  symgsssg  18587  symgfisg  18588  psgnunilem4  18617  odcong  18669  cmn4  18918  ablsub4  18926  abladdsub4  18927  lsm4  18973  abvdom  19602  abvres  19603  abvtrivd  19604  lspsolvlem  19907  lbsextlem2  19924  lidlsubcl  19982  frlmbas3  20465  matmulcell  21050  marrepeval  21168  ma1repveval  21176  submaeval  21187  mdetunilem3  21219  mdetuni0  21226  mdetmul  21228  minmar1eval  21254  nllyrest  22091  hausflimlem  22584  tsmsxp  22760  psmetlecl  22922  xmetlecl  22953  prdsxmetlem  22975  ngpocelbl  23310  bndth  23563  cph2ass  23818  iscau3  23882  dvres2  24515  coemullem  24847  vieta1  24908  aalioulem4  24931  cxpcn3lem  25336  angcan  25388  dchrvmasumlema  26084  logdivsum  26117  abvcxp  26199  padicabv  26214  ax5seglem3  26725  ax5seglem6  26728  axpasch  26735  axeuclid  26757  axcontlem4  26761  axcontlem8  26765  wlkl1loop  27427  trlsonwlkon  27499  pthontrlon  27536  wspthsswwlknon  27707  frgr2wwlkeqm  28116  adjlnop  29869  xreceu  30624  orngmul  30927  rhmdvd  30945  measvunilem  31581  measvunilem0  31582  measres  31591  bnj1128  32372  umgr2cycllem  32500  umgr2cycl  32501  satfv1fvfmla1  32783  fpr3g  33235  nosupbnd1lem4  33324  nosupbnd1lem5  33325  cgrcomim  33563  cgrcoml  33570  cgrcomr  33571  cgrdegen  33578  segconeu  33585  btwnintr  33593  btwnexch3  33594  btwnouttr2  33596  btwnouttr  33598  btwnexch  33599  trisegint  33602  lineext  33650  linecgr  33655  lineid  33657  idinside  33658  btwnconn1lem3  33663  btwnconn1lem4  33664  btwnconn1lem7  33667  btwnconn1lem14  33674  btwnconn2  33676  midofsegid  33678  btwnoutside  33699  outsideoftr  33703  lineunray  33721  lineelsb2  33722  cnres2  35201  heibor  35259  lsmcv2  36325  lcvat  36326  lcvexchlem4  36333  lcvexchlem5  36334  lfladd  36362  lflsub  36363  lflmul  36364  lshpkrlem4  36409  latm4  36529  omlmod1i2N  36556  cvlatexch3  36634  cvlsupr7  36644  hlatj4  36670  hlrelat3  36708  cvrval3  36709  atcvrj1  36727  atlelt  36734  2atlt  36735  2atjm  36741  3noncolr2  36745  athgt  36752  3dimlem2  36755  3dimlem4  36760  3dimlem4OLDN  36761  3dim3  36765  1cvratex  36769  ps-1  36773  ps-2  36774  hlatexch3N  36776  llnle  36814  atcvrlln2  36815  atcvrlln  36816  lplni2  36833  lplnle  36836  lplnnle2at  36837  llncvrlpln2  36853  lplnexllnN  36860  2llnmeqat  36867  lvolnle3at  36878  4atlem0ae  36890  lplncvrlvol2  36911  lnjatN  37076  lncvrat  37078  cdlemblem  37089  elpaddri  37098  paddasslem2  37117  paddasslem16  37131  padd4N  37136  hlmod1i  37152  dalawlem2  37168  pclfinN  37196  pexmidlem4N  37269  pl42lem1N  37275  lhp2lt  37297  lhpexle1  37304  lhpexle2lem  37305  lhpj1  37318  lhpmcvr5N  37323  lhp2at0  37328  lhp2atnle  37329  lhp2at0nle  37331  lhple  37338  lhpat  37339  lhpat4N  37340  4atexlempnq  37351  4atexlem7  37371  4atex  37372  ltrn11  37422  ltrnle  37425  ltrnm  37427  ltrnj  37428  ltrncvr  37429  ltrnel  37435  ltrncnvel  37438  ltrncnv  37442  trlval2  37459  trlcnv  37461  trljat1  37462  trljat2  37463  trlat  37465  trl0  37466  trlnidat  37469  trlnid  37475  cdlemc1  37487  cdlemc2  37488  cdlemc5  37491  cdlemd2  37495  cdlemd7  37500  cdlemd8  37501  cdlemd9  37502  cdleme0e  37513  cdleme3g  37530  cdleme3h  37531  cdleme3  37533  cdleme5  37536  cdleme10  37550  cdleme11a  37556  cdleme11c  37557  cdleme11h  37562  cdleme11j  37563  cdleme0nex  37586  cdleme18a  37587  cdleme18b  37588  cdleme22gb  37590  cdleme20zN  37597  cdleme20c  37607  cdleme20k  37615  cdleme21a  37621  cdleme21b  37622  cdleme21c  37623  cdleme21h  37630  cdleme22b  37637  cdleme22d  37639  cdleme22f  37642  cdleme25a  37649  cdleme25c  37651  cdleme25dN  37652  cdleme26ee  37656  cdleme30a  37674  cdlemefr29bpre0N  37702  cdlemefr29clN  37703  cdlemefr32fvaN  37705  cdlemefr32fva1  37706  cdlemefs29bpre0N  37712  cdlemefs29bpre1N  37713  cdlemefs29cpre1N  37714  cdlemefs29clN  37715  cdleme43fsv1snlem  37716  cdlemefs32fvaN  37718  cdlemefs32fva1  37719  cdlemefs31fv1  37720  cdleme36a  37756  cdleme39a  37761  cdleme42a  37767  cdleme42c  37768  cdleme17d3  37792  cdleme48fv  37795  cdleme48bw  37798  cdleme48b  37799  cdlemeg46rgv  37824  cdlemeg46req  37825  cdlemeg46gfv  37826  cdleme48d  37831  cdleme50trn2a  37846  cdleme50trn2  37847  cdleme50ltrn  37853  cdlemf1  37857  cdlemf  37859  trlord  37865  cdlemg2dN  37886  cdlemg2fvlem  37890  cdlemg2l  37899  cdlemg7fvbwN  37903  cdlemg7aN  37921  cdlemg10bALTN  37932  cdlemg10c  37935  cdlemg17a  37957  cdlemg17dALTN  37960  cdlemg31b0a  37991  cdlemg31a  37993  cdlemg31b  37994  cdlemg34  38008  cdlemg36  38010  ltrnco  38015  trlcoabs2N  38018  trlcolem  38022  cdlemg48  38033  tgrpov  38044  tendoco2  38064  tendoplco2  38075  cdlemh1  38111  cdlemi1  38114  cdlemi2  38115  cdlemj3  38119  tendoid0  38121  cdlemk1  38127  cdlemk2  38128  cdlemk4  38130  cdlemk8  38134  cdlemk9  38135  cdlemk9bN  38136  cdlemk10  38139  cdlemk26b-3  38201  cdlemk26-3  38202  cdlemk28-3  38204  cdlemk37  38210  cdlemk39  38212  cdlemkfid1N  38217  cdlemkid1  38218  cdlemky  38222  cdlemkyu  38223  cdlemk19ylem  38226  cdlemk19xlem  38238  cdlemk11t  38242  cdlemk51  38249  cdlemkyyN  38258  cdleml6  38277  cdleml7  38278  cdleml8  38279  cdleml9  38280  erngdvlem4  38287  erngdvlem4-rN  38295  tendospcanN  38319  dia11N  38344  cdlemm10N  38414  dib11N  38456  dicvaddcl  38486  dicvscacl  38487  cdlemn6  38498  dihvalcq2  38543  dihopelvalcpre  38544  dihord6b  38556  dihord5apre  38558  dihmeetlem1N  38586  dihmeetlem2N  38595  dihglbcpreN  38596  dihjatc1  38607  dihmeetlem20N  38622  dih1dimatlem0  38624  dihatlat  38630  dihglblem6  38636  dochexmidlem4  38759  mapdpglem32  39001  mapdh8ad  39075  mapdh9aOLDN  39086  hdmap11lem2  39138  hdmap14lem6  39169  frlmfzowrdb  39438  mzpsubst  39689  pellex  39776  pellfundex  39827  pellfund14gap  39828  qirropth  39849  rmxypos  39888  congmul  39908  congsub  39911  mzpcong  39913  coprmdvdsb  39926  jm2.15nn0  39944  jm2.16nn0  39945  rpnnen3lem  39972  idomsubgmo  40142  relexp01min  40414  mullimc  42258  islptre  42261  limccog  42262  mullimcf  42265  addlimc  42290  0ellimcdiv  42291  limsupre3lem  42374  stoweidlem57  42699  fourierdlem48  42796  fourierdlem80  42828  fourierdlem113  42861  ovncvrrp  43203  opnvonmbllem2  43272  ovolval5lem3  43293  ovnovollem3  43297  itsclc0lem1  45170  itsclc0lem2  45171  itschlc0yqe  45174  itscnhlc0xyqsol  45179  itschlc0xyqsol1  45180