Theorem simp1l 1194

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

Assertion

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

Proof of Theorem simp1l

Step	Hyp	Ref	Expression
1		simpl 486	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	3ad2ant1 1130	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:  simp11l  1281  simp21l  1287  simp31l  1293  tfisi  7553  offsplitfpar  7798  omeulem2  8192  uniinqs  8360  unxpdomlem3  8708  elfiun  8878  cantnffval  9110  tcrank  9297  cofsmo  9680  isfin2-2  9730  tskint  10196  tskun  10197  tskurn  10200  gruina  10229  dedekind  10792  subaddmulsub  11092  dmdcan  11339  lt2msq1  11513  supmullem1  11598  supmul  11600  xaddass  12630  xaddass2  12631  xlt2add  12641  xmulasslem3  12667  xadddi2r  12679  iccsplit  12863  expaddzlem  13468  expaddz  13469  expmulz  13471  ccatopth2  14070  pfxccat3  14087  resqrtcl  14605  limsupgle  14826  o1add  14962  o1mul  14963  o1sub  14964  bitsfzo  15774  sadfval  15791  smufval  15816  prmexpb  16052  4sqlem18  16288  vdwlem10  16316  fsets  16508  setsstruct2  16513  submre  16868  mrelatlub  17788  gsmsymgreqlem2  18551  mndodcong  18662  subgabl  18949  gex2abl  18964  cntzsubr  19561  abvres  19603  lbsind2  19846  lspsneu  19888  lbsextlem2  19924  lbsextg  19927  lindfind2  20507  matring  21048  maducoeval  21244  maducoeval2  21245  maduf  21246  madurid  21249  gsummatr01  21264  cramerimplem3  21290  cnprest  21894  hausnei2  21958  isreg2  21982  cmpcld  22007  llyrest  22090  nllyrest  22091  csdfil  22499  hausflimlem  22584  ssblps  23029  ssbl  23030  cphassi  23819  cphassir  23820  4cphipval2  23846  cphipval  23847  dvres2  24515  plyadd  24814  plymul  24815  coeeu  24822  vieta1  24908  aalioulem3  24930  aalioulem4  24931  efgh  25133  cxpadd  25270  cxpsub  25273  mulcxp  25276  divcxp  25278  cxple2  25288  cxplt2  25289  cxpcn3lem  25336  angcan  25388  ang180lem5  25399  isosctrlem3  25406  logexprlim  25809  lgssq  25921  abvcxp  26199  padicabv  26214  brbtwn2  26699  ax5seglem6  26728  axcontlem4  26761  axcontlem8  26765  uhgr2edg  26998  nbgrisvtx  27131  nbupgrres  27154  clwwlkccat  27775  clwwlknonex2lem2  27893  frgrreggt1  28178  chscllem4  29423  cshwrnid  30661  ogrpinvlt  30774  eqfunresadj  33117  poseq  33208  nosupbnd2lem1  33328  noetalem5  33334  ifscgr  33618  matunitlindflem1  35053  lshpnelb  36280  lfl1  36366  lshpkrlem6  36411  lshpkrex  36414  hlrelat3  36708  atbtwnexOLDN  36743  atbtwnex  36744  3dim3  36765  3atlem5  36783  2llnmat  36820  lvolex3N  36834  lvolnle3at  36878  4atlem11  36905  4atlem12  36908  dalemccea  36979  cdlema2N  37088  paddasslem2  37117  atmod1i1m  37154  lhp2lt  37297  lhp0lt  37299  lhpj1  37318  lhpmcvr4N  37322  lhpelim  37333  lhpmod2i2  37334  lhpmod6i1  37335  cdlemb2  37337  lhple  37338  lhpat  37339  4atex  37372  4atex2-0aOLDN  37374  4atex3  37377  ldilco  37412  ltrncl  37421  ltrn11  37422  ltrnle  37425  ltrncnvleN  37426  ltrnm  37427  ltrnj  37428  ltrncvr  37429  ltrnatb  37433  ltrnel  37435  ltrncnvel  37438  ltrncnv  37442  trlval2  37459  trlcnv  37461  trljat1  37462  trljat2  37463  trl0  37466  ltrnnidn  37470  trlnidatb  37473  cdlemc1  37487  cdlemc2  37488  cdlemc5  37491  cdlemc6  37492  cdlemd3  37496  cdlemd6  37499  cdleme0aa  37506  cdleme0b  37508  cdleme0c  37509  cdleme0e  37513  cdleme0fN  37514  cdleme01N  37517  cdleme02N  37518  cdleme0ex1N  37519  cdleme0moN  37521  cdleme3g  37530  cdleme3h  37531  cdleme3  37533  cdleme4  37534  cdleme4a  37535  cdleme5  37536  cdleme8  37546  cdleme9  37549  cdleme10  37550  cdleme16aN  37555  cdleme11a  37556  cdleme11fN  37560  cdleme11g  37561  cdleme11h  37562  cdleme11j  37563  cdleme11k  37564  cdleme12  37567  cdleme13  37568  cdleme17c  37584  cdleme17d1  37585  cdleme18a  37587  cdleme18b  37588  cdleme18c  37589  cdleme22gb  37590  cdlemeda  37594  cdlemednpq  37595  cdlemednuN  37596  cdleme19c  37601  cdleme20aN  37605  cdleme20bN  37606  cdleme20c  37607  cdleme22aa  37635  cdleme22a  37636  cdleme22b  37637  cdleme22d  37639  cdleme22e  37640  cdleme27cl  37662  cdleme27a  37663  cdleme30a  37674  cdleme42a  37767  cdleme42c  37768  cdleme50laut  37843  cdlemf1  37857  cdlemf  37859  cdlemfnid  37860  trlord  37865  cdlemg2fv2  37896  cdlemg2kq  37898  cdlemg2m  37900  cdlemg4a  37904  cdlemg4d  37909  cdlemg4g  37912  cdlemg4  37913  cdlemg6c  37916  cdlemg7aN  37921  cdlemg8a  37923  cdlemg8b  37924  cdlemg8c  37925  cdlemg9a  37928  cdlemg9b  37929  cdlemg9  37930  cdlemg11aq  37934  cdlemg10c  37935  cdlemg12a  37939  cdlemg12b  37940  cdlemg12c  37941  cdlemg17a  37957  cdlemg18b  37975  cdlemg18c  37976  cdlemg31b0a  37991  cdlemg31a  37993  cdlemg31b  37994  cdlemg31d  37996  cdlemg35  38009  trlcoabs2N  38018  trlcolem  38022  cdlemg44a  38027  trljco  38036  trljco2  38037  tendoco2  38064  tendopltp  38076  cdlemi1  38114  cdlemi2  38115  cdlemj3  38119  tendocan  38120  cdlemk3  38129  cdlemk4  38130  cdlemk5a  38131  cdlemk9  38135  cdlemk9bN  38136  cdlemkvcl  38138  cdlemk10  38139  cdlemk30  38190  cdlemk31  38192  cdlemk39  38212  cdlemkfid1N  38217  cdlemkid1  38218  cdlemkid2  38220  cdlemkfid3N  38221  cdlemk19ylem  38226  cdlemk19xlem  38238  cdlemk19x  38239  cdlemk53b  38252  cdlemk53  38253  cdlemk54  38254  cdlemk55a  38255  cdlemk43N  38259  cdlemk19u1  38265  cdlemk19u  38266  cdleml1N  38272  erngdvlem4  38287  erngdvlem4-rN  38295  dia11N  38344  cdlemm10N  38414  dib11N  38456  cdlemn2  38491  cdlemn10  38502  dihjustlem  38512  dihord2cN  38517  dihlsscpre  38530  dih1dimb2  38537  dihvalcq2  38543  dihopelvalcpre  38544  dihord6b  38556  dih11  38561  dihmeetlem1N  38586  dihglblem2N  38590  dihglblem3N  38591  dihmeetlem2N  38595  dihglbcpreN  38596  dihmeetcN  38598  dihmeetbclemN  38600  dihmeetlem4preN  38602  dihmeetlem9N  38611  dihmeetlem20N  38622  dihlspsnssN  38628  dihlspsnat  38629  dihatlat  38630  dihglblem6  38636  dihmeet  38639  dochss  38661  hdmapval3N  39134  hgmap11  39198  nn0rppwr  39490  remulcand  39575  congtr  39906  fzmaxdif  39922  isnumbasgrplem2  40048  ntrclsk13  40774  ssmapsn  41845  infleinf  42004  suplesup2  42008  supxrunb3  42036  mullimc  42258  mullimcf  42265  islpcn  42281  limsupresxr  42408  liminfresxr  42409  cncfuni  42528  icccncfext  42529  stoweidlem34  42676  stoweidlem59  42701  stirlinglem13  42728  fourierdlem41  42790  fourierdlem42  42791  fourierdlem73  42821  sge0iunmptlemfi  43052  meadjiunlem  43104  ovncvrrp  43203  sssmf  43372  smflimsuplem7  43457  smflimsuplem8  43458  funressneu  43639  lincscm  44839  lincext3  44865  el0ldep  44875  el0ldepsnzr  44876  itscnhlc0xyqsol  45179