Theorem simpll3 1095

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpll3	⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)

Proof of Theorem simpll3

Step	Hyp	Ref	Expression
1		simpl3 1059	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)
2	1	adantr 480	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  f1prex  6439  ordiso2  8303  wemappo  8337  iunfictbso  8820  fin1a2lem12  9116  fin1a2lem13  9117  prlem934  9734  ifle  11902  xlesubadd  11965  icoshftf1o  12166  elfzonelfzo  12436  fsuppmapnn0fiub0  12655  swrdcl  13271  repswccat  13383  subcn2  14173  rpdvds  15212  coprmprod  15213  qexpz  15443  ramval  15550  0ram  15562  cshwrepswhash1  15647  mreexexd  16131  mreexexdOLD  16132  gsumccat  17201  gsmsymgreqlem1  17673  pmtrf  17698  odmulg  17796  pgpfi1  17833  lsmcl  18904  lbsextlem3  18981  coe1mul2  19460  islindf4  19996  cramerlem2  20313  cpmadugsumlemF  20500  cayhamlem4  20512  iscnp4  20877  cnpnei  20878  cnconst2  20897  cnpdis  20907  cnhaus  20968  ordthauslem  20997  clscon  21043  nlly2i  21089  txcn  21239  ordthmeolem  21414  flimrest  21597  isfcf  21648  alexsubALTlem4  21664  ghmcnp  21728  utop2nei  21864  blssps  22039  blss  22040  metcnp3  22155  metcnp  22156  xrsxmet  22420  metdseq0  22465  xrhmeo  22553  cfil3i  22875  caucfil  22889  cfilres  22902  fta1b  23733  mumul  24707  lgsfcl2  24828  lgsdir  24857  lgsne0  24860  istrkgcb  25155  axbtwnid  25619  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  axcontlem8  25651  pjhthmo  27545  xrge0adddir  29023  archiabl  29083  pcmplfinf  29256  probun  29808  cnpcon  30466  outsideofeq  31407  linethru  31430  atlatmstc  33624  cvlcvr1  33644  ishlat3N  33659  hlrelat  33706  intnatN  33711  cvrval5  33719  atcvrlln  33824  llnexatN  33825  2at0mat0  33829  llncvrlpln  33862  lplnexllnN  33868  lplncvrlvol  33920  lncvrelatN  34085  pmapjoin  34156  pmapjat1  34157  pclclN  34195  osumclN  34271  lhprelat3N  34344  cdlemd5  34507  cdleme32fvcl  34746  cdlemg39  35022  ltrncom  35044  dihmeetALTN  35634  dochss  35672  mapdrvallem2  35952  nacsfix  36293  mzpsubst  36329  diophrw  36340  lzunuz  36349  jm2.19  36578  jm2.27  36593  hbtlem5  36717  iunrelexpuztr  37030  rfcnnnub  38218  3adantll2  38225  infleinf  38529  iccintsng  38596  mullimc  38683  mullimcf  38690  limcperiod  38695  cncfshift  38759  cncfperiod  38764  icccncfext  38773  stoweidlem20  38913  stoweidlem61  38954  fourierdlem73  39072  umgr2v2enb1  40742  wpthswwlks2on  41164  frgr3v  41445  frgr2wwlkeqm  41496  rmsupp0  41943  rmsuppss  41945