Theorem simprl 529

Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)

Assertion

Ref	Expression
simprl	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜓)

Proof of Theorem simprl

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad2antrl 490	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simp1rl  1062  simp2rl  1066  simp3rl  1070  rmob  3056  disjiun  3999  reg3exmidlemwe  4579  0xp  4707  imainss  5045  iotam  5209  fvmptt  5608  fcof1o  5790  isotr  5817  riota5f  5855  ovmpodf  6006  unielxp  6175  fnmpoovd  6216  1stconst  6222  2ndconst  6223  cnvf1olem  6225  tfrlemi14d  6334  tfrexlem  6335  tfr1onlemres  6350  tfrcllemres  6363  tfrcldm  6364  frecabcl  6400  nnaordi  6509  swoer  6563  qliftfun  6617  ecopovsymg  6634  th3qlem1  6637  mapen  6846  mapxpen  6848  fidifsnen  6870  fisbth  6883  findcard2d  6891  findcard2sd  6892  diffisn  6893  diffifi  6894  ac6sfi  6898  fimax2gtri  6901  fientri3  6914  nnwetri  6915  unsnfi  6918  unsnfidcex  6919  unsnfidcel  6920  fisseneq  6931  fidcenumlemrk  6953  fidcenumlemr  6954  isbth  6966  ordiso2  7034  difinfsnlem  7098  difinfinf  7100  ctmlemr  7107  ctssdccl  7110  fodjum  7144  fodju0  7145  omniwomnimkv  7165  exmidfodomrlemrALT  7202  netap  7253  exmidmotap  7260  cc1  7264  cc2lem  7265  cc3  7267  cc4f  7268  cc4n  7270  dfplpq2  7353  dfmpq2  7354  mulpipqqs  7372  distrnqg  7386  ltexnqq  7407  subhalfnqq  7413  distrnq0  7458  prarloclemup  7494  prarloclem3  7496  prarloc  7502  genplt2i  7509  nqprl  7550  nqpru  7551  prmuloc  7565  mullocpr  7570  distrlem4prl  7583  distrlem4pru  7584  ltaddpr  7596  ltexprlemopl  7600  ltexprlemlol  7601  ltexprlemopu  7602  ltexprlemupu  7603  ltexprlemrl  7609  ltexprlemru  7611  addcanprleml  7613  addcanprlemu  7614  ltaprlem  7617  ltaprg  7618  prplnqu  7619  addextpr  7620  recexprlemdisj  7629  recexprlemloc  7630  recexprlem1ssl  7632  aptiprleml  7638  aptiprlemu  7639  ltmprr  7641  archpr  7642  cauappcvgprlemopl  7645  cauappcvgprlemopu  7647  cauappcvgprlemdisj  7650  cauappcvgprlemloc  7651  cauappcvgprlem1  7658  cauappcvgprlem2  7659  cauappcvgprlemlim  7660  caucvgprlemnkj  7665  caucvgprlemopl  7668  caucvgprlemopu  7670  caucvgprlemdisj  7673  caucvgprlemloc  7674  caucvgprlem2  7679  caucvgprprlemnkltj  7688  caucvgprprlemnkeqj  7689  caucvgprprlemnjltk  7690  caucvgprprlemmu  7694  caucvgprprlemopl  7696  caucvgprprlemopu  7698  caucvgprprlemdisj  7701  caucvgprprlemloc  7702  caucvgprprlemexbt  7705  caucvgprprlemaddq  7707  caucvgprprlem2  7709  suplocexprlemrl  7716  suplocexprlemmu  7717  suplocexprlemru  7718  suplocexprlemdisj  7719  suplocexprlemloc  7720  suplocexprlemex  7721  suplocexprlemub  7722  suplocexprlemlub  7723  recexgt0sr  7772  mulgt0sr  7777  prsrriota  7787  caucvgsrlemoffres  7799  suplocsrlem  7807  cnm  7831  addcnsr  7833  mulcnsr  7834  mulcnsrec  7842  axaddcl  7863  axmulcl  7865  axmulcom  7870  rereceu  7888  recriota  7889  axcaucvglemres  7898  axpre-suploclemres  7900  lelttr  8046  ltletr  8047  readdcan  8097  addcan  8137  addcan2  8138  addsub4  8200  ltadd2  8376  le2add  8401  lt2add  8402  lt2sub  8417  le2sub  8418  eqord1  8440  rimul  8542  rereim  8543  ltmul1  8549  apreim  8560  mulreim  8561  apcotr  8564  apadd1  8565  addext  8567  apneg  8568  mulext1  8569  mulext  8571  ltleap  8589  aprcl  8603  mulap0  8611  mulcanapd  8618  receuap  8626  recapb  8628  rec11ap  8667  rec11rap  8668  divdivdivap  8670  ddcanap  8683  divadddivap  8684  conjmulap  8686  subrecap  8796  prodgt0gt0  8808  prodge0  8811  ltmul12a  8817  lemulge11  8823  lt2mul2div  8836  ltrec  8840  lerec  8841  lt2msq  8843  lerec2  8846  le2msq  8858  msq11  8859  ledivp1  8860  mulle0r  8901  suprzclex  9351  peano5uzti  9361  supinfneg  9595  infsupneg  9596  qapne  9639  xrlelttr  9806  xrltletr  9807  xrre  9820  xaddge0  9878  xle2add  9879  xlt2add  9880  divelunit  10002  fzass4  10062  fzocatel  10199  exbtwnzlemex  10250  rebtwn2z  10255  qbtwnre  10257  modqid  10349  modqcyc  10359  modqaddabs  10362  modqaddmod  10363  mulqaddmodid  10364  modqadd2mod  10374  modqltm1p1mod  10376  modqsubmod  10382  modqsubmodmod  10383  modqmulmod  10389  modqmulmodr  10390  modqaddmulmod  10391  modqsubdir  10393  frec2uzisod  10407  iseqovex  10456  seqvalcd  10459  seqf  10461  seqovcd  10463  seq3fveq2  10469  seq3shft2  10473  monoord  10476  seq3split  10479  iseqf1olemnab  10488  seq3id2  10509  seq3distr  10513  expcl2lemap  10532  expnegzap  10554  ltexp2a  10572  le2sq2  10596  nn0ltexp2  10689  nn0opth2  10704  bcval5  10743  hashcl  10761  hashen  10764  fihashdom  10783  hashunlem  10784  hashun  10785  fimaxq  10807  zfz1isolem1  10820  zfz1iso  10821  cvg1nlemres  10994  cvg1n  10995  recvguniq  11004  resqrexlemp1rp  11015  resqrexlemoverl  11030  resqrexlemglsq  11031  resqrexlemex  11034  sqrtmul  11044  sqrtsq  11053  absexpzap  11089  absle  11098  abs3lem  11120  amgm2  11127  maxleastlt  11224  maxltsup  11227  fimaxre2  11235  xrmaxleastlt  11264  xrmaxltsup  11266  xrmaxaddlem  11268  climcn2  11317  addcn2  11318  mulcn2  11320  reccn2ap  11321  climcau  11355  summodclem2  11390  summodc  11391  fsumf1o  11398  fisumss  11400  fsum3cvg3  11404  fsumcl2lem  11406  fsumadd  11414  fsum2dlemstep  11442  mptfzshft  11450  fsumrev  11451  fsummulc2  11456  modfsummod  11466  fsumrelem  11479  binom  11492  cvgratnn  11539  mertenslemub  11542  prodmodc  11586  zproddc  11587  fprodf1o  11596  fprodssdc  11598  fprodmul  11599  fprodrev  11627  fprod2dlemstep  11630  efcllem  11667  tanaddaplem  11746  dvdsval2  11797  moddvds  11806  dvdsabseq  11853  dvdsflip  11857  oexpneg  11882  fldivndvdslt  11940  zsupcllemstep  11946  zssinfcl  11949  suprzubdc  11953  zsupssdc  11955  suprzcl2dc  11956  bezoutlemnewy  11997  bezoutlemstep  11998  bezoutlemeu  12008  dfgcd3  12011  bezout  12012  dvdsmulgcd  12026  bezoutr  12033  ialgrlem1st  12042  lcmgcdlem  12077  coprmdvds2  12093  qredeu  12097  rpdvds  12099  isprm5lem  12141  isprm6  12147  pw2dvdslemn  12165  nonsq  12207  crth  12224  eulerthlemh  12231  pclemdc  12288  pcprendvds2  12291  pceu  12295  pcval  12296  pczpre  12297  pcmul  12301  pcqmul  12303  pcqcl  12306  pcid  12323  pcneg  12324  pcgcd1  12327  pc2dvds  12329  pcprmpw2  12332  difsqpwdvds  12337  pcmpt  12341  pockthg  12355  1arith  12365  mul4sq  12392  ennnfonelemg  12404  ennnfonelemex  12415  ennnfonelemrnh  12417  ennnfonelemrn  12420  ennnfonelemdm  12421  ennnfonelemnn0  12423  ennnfonelemim  12425  ennnfone  12426  ctinfomlemom  12428  ctinf  12431  ctiunctlemfo  12440  nninfdclemcl  12449  nninfdclemf  12450  nninfdclemp1  12451  unbendc  12455  isstruct2r  12473  setscom  12502  qusval  12744  ercpbl  12750  opifismgmdc  12790  grprinvlem  12804  grpridd  12806  mndpropd  12841  issubmnd  12843  submnd0  12845  mhmf1o  12861  0mhm  12873  mhmco  12874  mhmima  12875  mhmeql  12876  grppropd  12893  grpinvid1  12924  grpinvid2  12925  grplcan  12932  grplmulf1o  12944  grpnpncan0  12966  dfgrp3mlem  12968  grplactcnv  12972  mulgval  12986  mulgfng  12987  mulg1  12990  mulgnnp1  12991  mulgneg  13001  mulgnndir  13012  mulgdirlem  13014  mulgnn0ass  13019  mulgass  13020  subgmulg  13048  issubg4m  13053  subgintm  13058  0nsg  13074  eqgcpbl  13087  ablpncan3  13120  srglmhm  13176  srgrmhm  13177  ringpropd  13217  dvdsrvald  13262  dvdsrd  13263  dvdsrex  13267  dvdsrtr  13270  unitgrp  13285  unitpropdg  13317  subrgintm  13364  aprap  13376  lmodprop2d  13438  rmodislmodlem  13440  epttop  13593  topssnei  13665  restbasg  13671  restopnb  13684  cnfval  13697  cnpfval  13698  iscnp4  13721  cnpnei  13722  cnptopco  13725  cncnp  13733  cnrest2  13739  cnptoprest  13742  cnptoprest2  13743  lmss  13749  lmtopcnp  13753  neitx  13771  txcnp  13774  txrest  13779  txdis  13780  txlm  13782  cnmpt21  13794  imasnopn  13802  xmetres2  13882  blvalps  13891  blval  13892  bl2in  13906  blhalf  13911  blssps  13930  blss  13931  blssexps  13932  blssex  13933  ssblex  13934  blin2  13935  metss2lem  14000  bdmetval  14003  bdmopn  14007  metrest  14009  xmetxp  14010  xmetxpbl  14011  xmettx  14013  metcnp3  14014  txmetcnp  14021  addcncntoplem  14054  elcncf2  14064  mulc1cncf  14079  cncfco  14081  cncfmet  14082  mulcncf  14094  dedekindeulemub  14099  dedekindeulemloc  14100  dedekindeulemlu  14102  dedekindeu  14104  suplociccex  14106  dedekindicclemub  14108  dedekindicclemloc  14109  dedekindicclemlu  14111  dedekindicc  14114  ivthinclemlopn  14117  ivthinclemuopn  14119  ivthdec  14125  limcimolemlt  14136  limcimo  14137  cnplimccntop  14142  limccnp2lem  14148  limccnp2cntop  14149  dvfvalap  14153  dveflem  14190  reeff1olem  14195  reeff1oleme  14196  eflt  14199  sin0pilem2  14206  pilem3  14207  ptolemy  14248  ioocosf1o  14278  cxplt  14339  cxple  14340  cxplt3  14343  apcxp2  14361  rprelogbmul  14376  rprelogbdiv  14378  logbgt0b  14387  logbgcd1irrap  14391  lgsdir2lem5  14436  lgsdir  14439  lgsdi  14441  lgsne0  14442  lgseisenlem2  14454  2sqlem6  14470  2sqlem10  14475  nnti  14747  pwtrufal  14750  pwf1oexmid  14752  sssneq  14754  qdencn  14778  cvgcmp2n  14784  trilpolemlt1  14792  trirec0  14795  trirec0xor  14796  redc0  14808  reap0  14809  nconstwlpolemgt0  14814  neap0mkv  14819  supfz  14821  inffz  14822