Theorem simplrl 774

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

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

Proof of Theorem simplrl

Step	Hyp	Ref	Expression
1		simpl 483	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antlr 724	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  disjxiun  5072  frpomin  6247  f1imass  7146  f1prex  7165  soisoi  7208  riota5f  7270  tfrlem9a  8226  oeeui  8442  oaabs2  8488  omabs  8490  omxpenlem  8869  fopwdom  8876  frfi  9068  marypha1lem  9201  ordiso2  9283  oismo  9308  wemaplem3  9316  cantnf  9460  ttrclss  9487  isinffi  9759  dfac12lem2  9909  dfac12lem3  9910  infxp  9980  infmap2  9983  infpssrlem5  10072  fin23lem11  10082  fin23lem24  10087  fin23lem26  10090  isf32lem2  10119  isf32lem4  10121  fin1a2lem13  10177  fin1a2s  10179  ttukeylem5  10278  fpwwe2lem11  10406  fpwwe2lem12  10407  wunex2  10503  tskord  10545  prlem934  10798  mulcmpblnr  10836  dedekind  11147  addid1  11164  cnegex  11165  negeu  11220  add20  11496  divdivdiv  11685  ltmul12a  11840  lediv12a  11877  cru  11974  uzwo3  12692  xleadd1a  12996  xlemul1a  13031  ixxun  13104  ixxss12  13108  elfz0ubfz0  13369  mulexpz  13832  rpexpmord  13895  leexp1a  13902  expmulnbnd  13959  swrdccatin1  14447  pfxccatin12lem3  14454  pfxccat3  14456  abs3lem  15059  rexanre  15067  cau3lem  15075  lo1bdd2  15242  o1lo1  15255  rlimclim1  15263  rlimclim  15264  lo1resb  15282  o1resb  15284  rlimcn3  15308  o1of2  15331  o1rlimmul  15337  lo1add  15345  lo1mul  15346  isercolllem1  15385  climcau  15391  summolem2  15437  summo  15438  o1fsum  15534  prodmolem2  15654  qredeu  16372  isprm5  16421  pclem  16548  pcqmul  16563  pcexp  16569  pcneg  16584  pcprmpw2  16592  pcadd  16599  prmpwdvds  16614  4sqlem13  16667  vdwlem2  16692  vdwlem7  16697  vdwlem11  16701  vdwlem12  16702  ramval  16718  ramz2  16734  ramcl  16739  prmgaplem6  16766  cshwshashlem2  16807  imasval  17231  imasdsval  17235  mreexexd  17366  issubc3  17573  idfucl  17605  funcres2c  17626  fucpropd  17704  xpcval  17903  prfval  17925  evlfcl  17949  curf12  17954  curf1cl  17955  curf2  17956  curfcl  17959  curfuncf  17965  curf2ndf  17974  hof2val  17983  hofcl  17986  hofpropd  17994  yonedalem4a  18002  yonedainv  18008  poslubmo  18138  posglbmo  18139  isipodrs  18264  acsmapd  18281  acsinfd  18283  ismndd  18416  mndpropd  18419  mhmeql  18473  mndind  18475  frmdup3lem  18514  mhmmnd  18706  issubg4  18783  ssnmz  18803  f1otrspeq  19064  psgneu  19123  sylow2blem3  19236  lsmdisj2  19297  pj1eu  19311  efgredlem  19362  frgpuplem  19387  frgpnabl  19485  dmdprdsplitlem  19649  pgpfac1lem3  19689  pgpfaclem3  19695  ablsimpgcygd  19718  ringpropd  19830  dvdsrtr  19903  islmhm2  20309  lmhmpropd  20344  prmirredlem  20703  psgndiflemA  20815  lsmcss  20906  dsmmlss  20960  uvcf1  21008  frlmup1  21014  assapropd  21085  evlslem1  21301  coe1tmmul2  21456  mamucl  21557  mamuass  21558  mamudi  21559  mamudir  21560  mamuvs1  21561  mamuvs2  21562  mamulid  21599  mamurid  21600  dmatsubcl  21656  dmatmulcl  21658  mdetunilem7  21776  mdetunilem9  21778  cramer0  21848  cpmatmcllem  21876  mat2pmatf1  21887  decpmatmul  21930  pmatcollpw1  21934  pm2mpf1lem  21952  pm2mpmhmlem2  21977  chpidmat  22005  cpmadugsumlemB  22032  cpmadugsumlemC  22033  toponmre  22253  restbas  22318  iscncl  22429  cnpdis  22453  lmcnp  22464  dishaus  22542  cmpcovf  22551  hauscmplem  22566  dfconn2  22579  clsconn  22590  2ndcctbss  22615  1stccnp  22622  islly2  22644  llyidm  22648  cldllycmp  22655  locfincmp  22686  kgentopon  22698  1stckgenlem  22713  ptpjpre1  22731  ptbasfi  22741  txcls  22764  ptpjopn  22772  xkoccn  22779  txcnp  22780  txcmpb  22804  xkoptsub  22814  xkoco2cn  22818  xkoinjcn  22847  qtopcn  22874  qtoprest  22877  regr1lem  22899  regr1lem2  22900  kqreglem1  22901  qtophmeo  22977  fgabs  23039  hauspwpwf1  23147  flimfnfcls  23188  fclscmp  23190  cnpfcf  23201  ptcmplem4  23215  ptcmplem5  23216  cnextfval  23222  cnextfun  23224  tmdgsum2  23256  tsmsval2  23290  utoptop  23395  utop3cls  23412  ismet2  23495  blin  23583  metss2lem  23676  methaus  23685  met1stc  23686  met2ndci  23687  metcnp  23706  metcnpi3  23711  metustto  23718  metustfbas  23722  nlmvscn  23860  nrginvrcn  23865  nghmcn  23918  xrsxmet  23981  reconnlem1  23998  reconn  24000  xrge0tsms  24006  xmetdcn2  24009  metdscn  24028  addcnlem  24036  mulc1cncf  24077  cncfco  24079  cnheiborlem  24126  cnheibor  24127  nmoleub2lem2  24288  ipcn  24419  iscfil3  24446  cfilfcls  24447  iscmet3  24466  caubl  24481  bcthlem5  24501  rrxdstprj1  24582  minveclem3b  24601  minveclem7  24608  pmltpc  24623  ovolshftlem1  24682  ovolscalem1  24686  ioombl1  24735  uniioombllem6  24761  dyadss  24767  dyaddisjlem  24768  dyadmax  24771  opnmbllem  24774  itg1addlem2  24870  itg2seq  24916  bddmulibl  25012  limcfval  25045  ellimc3  25052  limciun  25067  dveflem  25152  rolle  25163  dvlip2  25168  c1liplem1  25169  dvgt0lem1  25175  dvgt0  25177  dvlt0  25178  dvne0  25184  dvcnvre  25192  dvfsumrlimge0  25203  ftc1lem6  25214  itgsubst  25222  mdegmullem  25252  ply1domn  25297  fta1g  25341  fta1b  25343  dgrlem  25399  coeid  25408  plydivalg  25468  aannenlem1  25497  aalioulem6  25506  ulmcn  25567  mtestbdd  25573  abelthlem8  25607  efif1olem4  25710  chordthm  25996  xrlimcnp  26127  lgamgulmlem5  26191  isppw2  26273  fsumvma2  26371  perfectlem2  26387  lgsdilem  26481  lgsquad2lem2  26542  lgsquad3  26544  2sqlem5  26579  2sqlem9  26584  rpvmasumlem  26644  dchrisum0flb  26667  pntpbnd  26745  pntibndlem3  26749  pntlem3  26766  pntleml  26768  tgjustc1  26845  tgjustc2  26846  tgbtwnconn1lem3  26944  legtrid  26961  tglinethru  27006  tglnpt2  27011  tglineintmo  27012  mirreu3  27024  perpcom  27083  footexALT  27088  footex  27091  mideu  27108  opphllem1  27117  lnopp2hpgb  27133  axsegcon  27304  axpasch  27318  axeuclidlem  27339  ecgrtg  27360  elntg  27361  eengtrkg  27363  upgr1eopALT  27496  usgredg4  27593  usgr1eop  27626  usgr1v  27632  subuhgr  27662  subumgr  27664  subusgr  27665  nbuhgr2vtx1edgb  27728  wwlksnext  28267  usgr2wspthon  28339  clwlkclwwlkf1  28383  clwwisshclwwslem  28387  n4cyclfrgr  28664  dlwwlknondlwlknonf1o  28738  vacn  29065  ubthlem1  29241  ubthlem3  29243  minvecolem7  29254  chocunii  29672  pjhthmo  29673  pjhthlem2  29763  nmopub2tALT  30280  nmfnleub2  30297  kbass5  30491  mdslmd1lem1  30696  mdslmd1lem2  30697  mdsymlem5  30778  fcobij  31066  xrofsup  31099  mgcf1o  31290  xrge0tsmsd  31326  symgcntz  31363  archiabllem2a  31457  gsumvsca1  31488  gsumvsca2  31489  isarchiofld  31525  prmidl2  31625  ssmxidl  31651  smatrcl  31755  reff  31798  ordtconnlem1  31883  qqhval2  31941  esumpcvgval  32055  imambfm  32238  ballotlemsf1o  32489  signstfvneq0  32560  pconnconn  33202  connpconn  33206  cvmliftmo  33255  cvmlift2lem10  33283  cvmlift2lem12  33285  cvmlift3lem7  33296  mrsubff1  33485  msubff1  33527  frxp3  33806  naddssim  33846  nosupbday  33917  noinfbday  33932  noetasuplem4  33948  noetainflem4  33952  noetalem1  33953  slerec  34022  madebdaylemlrcut  34088  ifscgr  34355  cgrxfr  34366  btwnconn1lem13  34410  ellines  34463  unblimceq0lem  34695  unbdqndv2  34700  irrdiff  35506  matunitlindflem1  35782  poimirlem4  35790  poimirlem13  35799  poimirlem14  35800  heicant  35821  opnmbllem0  35822  mblfinlem3  35825  itg2addnclem  35837  itg2addnc  35840  ftc1cnnc  35858  sstotbnd  35942  cntotbnd  35963  ismtyima  35970  heibor1lem  35976  heiborlem10  35987  bfp  35991  rrncmslem  35999  islshpsm  37001  lsatcmp  37024  islshpat  37038  lfl0f  37090  iscvlat2N  37345  ishlat3N  37375  3dim1  37488  islvol5  37600  lvoli2  37602  lncvrelatN  37802  lncmp  37804  paddasslem10  37850  pclfinclN  37971  pexmidlem8N  37998  idltrn  38171  cdleme42keg  38507  cdleme42mgN  38509  cdlemf2  38583  cdlemg2cex  38612  trlcoat  38744  tendoex  38996  erngdvlem4  39012  erngdvlem4-rN  39020  dialss  39067  dibglbN  39187  diblss  39191  dihlsscpre  39255  dihglblem2aN  39314  dihglblem4  39318  dihglblem5  39319  dih1dimatlem  39350  dihglblem6  39361  lcfl7N  39522  lcfrlem9  39571  mapdh9a  39810  hdmapglem7  39950  aks4d1p8  40102  sticksstones22  40131  fsuppind  40286  renegeulemv  40358  sn-subeu  40415  remulinvcom  40421  itrere  40443  retire  40444  prjspertr  40451  prjspreln0  40455  flt4lem7  40503  nna4b4nsq  40504  isnacs3  40539  nacsfix  40541  mzpsubst  40577  eldioph2lem2  40590  eldioph2  40591  eldioph2b  40592  diophin  40601  diophun  40602  rencldnfilem  40649  irrapxlem3  40653  irrapxlem5  40655  pell1234qrreccl  40683  pell1234qrmulcl  40684  pell1qrge1  40699  pell1qrgaplem  40702  monotuz  40770  monotoddzzfi  40771  acongtr  40807  acongrep  40809  jm2.26a  40829  jm2.26lem3  40830  jm2.26  40831  jm2.27b  40835  jm2.27  40837  wepwsolem  40874  fnwe2lem2  40883  hbtlem5  40960  hbt  40962  mpaaeu  40982  rfovcnvf1od  41619  mnurndlem1  41906  fnchoice  42579  rfcnnnub  42586  disjxp1  42624  ioondisj2  43038  iccintsng  43068  fprodcn  43148  lptioo2  43179  lptioo1  43180  limclner  43199  dvdsn1add  43487  stoweidlem14  43562  stoweidlem27  43575  stoweidlem34  43582  stoweidlem49  43597  stoweidlem56  43604  fourierdlem87  43741  iundjiun  44005  ismeannd  44012  hoidmvle  44145  prproropf1olem2  44967  perfectALTVlem2  45185  mogoldbb  45248  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  mgmhmeql  45368  rngcinv  45550  rngcinvALTV  45562  ringcinv  45601  ringcinvALTV  45625  mndpsuppss  45718  lindslinindsimp2lem5  45814  itscnhlinecirc02p  46142  toslat  46279  functhinclem4  46336