Theorem simp3r 1221

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

Assertion

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

Proof of Theorem simp3r

Step	Hyp	Ref	Expression
1		simpr 490	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	3ad2ant3 1153	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp13r  1308  simp23r  1314  simp33r  1320  f1oiso2  7361  tfisi  7871  tfrlem5  8391  omeulem1  8594  omeulem2  8595  elfiun  9426  isfin2-2  10401  addlid  11497  mulcan  11957  mulcan2  11958  divass  11996  divdir  12003  ltdiv1  12185  ltmuldiv  12194  lediv2  12211  xaddass2  13384  xlt2add  13394  expaddz  14253  expmulz  14255  resqrex  15423  resqrtcl  15426  o1add  15787  o1mul  15788  o1sub  15789  dvdsgcd  16723  rpexp12i  16906  pythagtriplem4  17003  pythagtriplem11  17009  pythagtriplem13  17011  pcpremul  17027  pceu  17030  pcqmul  17037  pcqdiv  17041  f1ocpbllem  17702  funcoppc  18056  funcres  18077  catcisolem  18291  1stfcl  18377  2ndfcl  18378  prfcl  18383  evlfcl  18402  curf1cl  18408  curfcl  18412  hofcl  18439  latjlej12  18635  latmlem12  18651  latj4  18669  latj4rot  18670  symgsssg  19687  symgfisg  19688  odcong  19769  cmn4  20021  ablsub4  20030  abladdsub4  20031  lsm4  20080  abvdom  21093  abvtrivd  21095  orngmul  21128  lspsolvlem  21426  lbsextlem2  21443  lidlsubcl  21509  frlmbas3  22088  matinvgcell  22756  matmulcell  22766  ma1repveval  22892  mdetunilem3  22935  mdetuni0  22942  mdetmul  22944  hausflimlem  24304  psmetlecl  24640  xmetlecl  24671  prdsxmetlem  24693  xblcntrps  24735  xblcntr  24736  bndth  25285  cph2ass  25540  iscau3  25605  dvres2  26238  coemullem  26575  vieta1  26641  aalioulem4  26668  cxpcn3lem  27081  angcan  27136  divsqrtsumlem  27313  dchrmusumlema  27826  dchrvmasumlema  27833  dchrisum0lema  27847  logdivsum  27866  padicabv  27963  cofcut1  28312  cofcut2  28314  divmulsw  28585  precsexlem8  28606  precsexlem9  28607  bdayfinbndlem1  28859  ax5seglem3  29515  ax5seglem6  29518  axpasch  29525  axeuclid  29547  axcontlem4  29551  axcontlem8  29555  trlsonistrl  30297  pthonispth  30338  spthonisspth  30342  wspthneq1eq2  30455  umgr2cycllem  30752  umgr2cycl  30753  frgr2wwlkeqm  30938  adjlnop  32694  xreceu  33535  rhmdvd  33932  measvunilem  34892  measvuni  34894  bnj1128  35667  satfv1fvfmla1  36275  cgrcomim  36847  cgrcoml  36854  cgrcomr  36855  cgrdegen  36862  segconeu  36869  btwnintr  36877  btwnexch3  36878  btwnouttr2  36880  btwnouttr  36882  btwnexch  36883  ifscgr  36902  lineext  36934  linecgr  36939  lineid  36941  idinside  36942  btwnconn1lem3  36947  btwnconn1lem4  36948  btwnconn1lem14  36958  btwnconn2  36960  btwnconn3  36961  midofsegid  36962  btwnoutside  36983  outsideoftr  36987  lineunray  37005  lineelsb2  37006  itg2addnclem  38683  cnres2  38791  heibor  38849  lsmcv2  40180  lcvat  40181  lcvexchlem4  40188  lcvexchlem5  40189  lfladd  40217  lflsub  40218  lflmul  40219  lshpkrlem4  40264  latm4  40384  omlmod1i2N  40411  cvlsupr7  40499  cvlsupr8  40500  hlatj4  40525  hlrelat3  40563  cvrval3  40564  atcvrj1  40582  atlelt  40589  2atlt  40590  2atjm  40596  3noncolr2  40600  athgt  40607  3dimlem2  40610  3dimlem4OLDN  40616  1cvratex  40624  ps-1  40628  ps-2  40629  hlatexch3N  40631  llnle  40669  atcvrlln2  40670  atcvrlln  40671  lplni2  40688  lplnle  40691  lplnnle2at  40692  lplnnlelln  40694  llncvrlpln2  40708  2llnmeqat  40722  lvolnle3at  40733  lvolnlelln  40735  4atlem0ae  40745  lneq2at  40929  lnjatN  40931  lncvrat  40933  2lnat  40935  elpaddri  40953  paddasslem2  40972  padd4N  40991  hlmod1i  41007  llnexchb2  41020  dalawlem2  41023  pclfinN  41051  pexmidlem4N  41124  pl42lem1N  41130  lhp2lt  41152  lhpexle1  41159  lhpexle2lem  41160  lhpj1  41173  lhpmcvr5N  41178  lhp2at0  41183  lhp2at0nle  41186  lhple  41193  lhpat  41194  lhpat4N  41195  4atexlemnslpq  41207  4atexlem7  41226  ltrn11  41277  ltrnle  41280  ltrnm  41282  ltrnj  41283  ltrncvr  41284  ltrnel  41290  ltrncnvel  41293  ltrncnv  41297  trlat  41320  trl0  41321  trlnidat  41324  trlnid  41330  ltrnatlw  41334  trlne  41336  trlval4  41339  cdlemc5  41346  cdlemd2  41350  cdlemd7  41355  cdlemd8  41356  cdlemd9  41357  cdleme0c  41364  cdleme0e  41368  cdleme0fN  41369  cdleme3g  41385  cdleme3h  41386  cdleme5  41391  cdleme11c  41412  cdleme11h  41417  cdleme11j  41418  cdleme11k  41419  cdleme0nex  41441  cdleme18a  41442  cdleme22gb  41445  cdleme20zN  41452  cdleme20c  41462  cdleme20k  41470  cdleme21a  41476  cdleme21b  41477  cdleme21c  41478  cdleme21ct  41480  cdleme21h  41485  cdleme22d  41494  cdleme22f  41497  cdleme26ee  41511  cdleme30a  41529  cdlemefs45eN  41582  cdleme36a  41611  cdleme36m  41612  cdleme39a  41616  cdleme42b  41629  cdleme43dN  41643  cdlemeg47rv2  41661  cdlemeg46sfg  41671  cdlemeg46rjgN  41673  cdlemeg46rgv  41679  cdlemeg46req  41680  cdlemeg46gfv  41681  cdleme48d  41686  cdleme50ltrn  41708  cdlemf1  41712  cdlemf  41714  cdlemg2dN  41741  cdlemg2fvlem  41745  cdlemg2l  41754  cdlemg7fvbwN  41758  cdlemg7aN  41776  cdlemg10c  41790  cdlemg17a  41812  cdlemg17dALTN  41815  cdlemg18a  41829  cdlemg18b  41830  cdlemg31b0a  41846  cdlemg31a  41848  cdlemg31b  41849  ltrnco  41870  cdlemg48  41888  tgrpov  41899  tendoco2  41919  tendoplco2  41930  cdlemh1  41966  cdlemk1  41982  cdlemk26b-3  42056  cdlemk27-3  42058  cdlemk28-3  42059  cdlemk34  42061  cdlemkfid1N  42072  cdlemkid3N  42084  cdlemkid4  42085  cdlemk35s-id  42089  cdlemk39s-id  42091  cdlemk51  42104  tendospcanN  42174  cdlemm10N  42269  dicvaddcl  42341  dicvscacl  42342  cdlemn6  42353  dihvalcq2  42398  dihord6b  42411  dihord5apre  42413  dihglbcpreN  42451  dihjatc1  42462  dihmeetlem20N  42477  dih1dimatlem0  42479  dihglblem6  42491  dochexmidlem4  42614  mapdpglem32  42856  mapdh8ad  42930  mapdh9aOLDN  42941  hdmap11lem2  42993  hdmap14lem6  43024  frlmfzowrdb  43665  mzpmfp  43852  mzpsubst  43853  pellex  43936  pellfundex  43987  pellfund14gap  43988  qirropth  44009  rmxypos  44048  congmul  44068  congsub  44071  mzpcong  44073  coprmdvdsb  44086  jm2.15nn0  44104  jm2.16nn0  44105  rpnnen3lem  44132  idomsubgmo  44289  relexp01min  44807  mullimc  46722  islptre  46725  mullimcf  46729  addlimc  46752  0ellimcdiv  46753  limsupre3lem  46836  limsupre3uzlem  46839  fourierdlem48  47258  fourierdlem80  47290  opnvonmbllem2  47737  ovolval5lem3  47758  ovnovollem3  47762  difltmodne  48512  isubgr3stgrlem1  49158  grlimedgclnbgr  49187  mapprop  49552  lincfsuppcl  49619  lindslinindimp2lem3  49666  itsclc0lem1  49962  itsclc0lem2  49963  itschlc0yqe  49966  itsclc0xyqsolr  49975  swapffunc  50498  fucofunc  50575  fucoppc  50639  parmapfunc2  50868  parmapfunc  50869