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 489	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	3ad2ant3 1153	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  simp13r  1308  simp23r  1314  simp33r  1320  f1oiso2  7352  tfisi  7856  tfrlem5  8367  omeulem1  8568  omeulem2  8569  elfiun  9391  isfin2-2  10304  addlid  11394  mulcan  11852  mulcan2  11853  divass  11891  divdir  11898  ltdiv1  12080  ltmuldiv  12089  lediv2  12106  xaddass2  13277  xlt2add  13287  expaddz  14144  expmulz  14146  resqrex  15303  resqrtcl  15306  o1add  15667  o1mul  15668  o1sub  15669  dvdsgcd  16603  rpexp12i  16784  pythagtriplem4  16880  pythagtriplem11  16886  pythagtriplem13  16888  pcpremul  16904  pceu  16907  pcqmul  16914  pcqdiv  16918  f1ocpbllem  17579  funcoppc  17933  funcres  17954  catcisolem  18168  1stfcl  18254  2ndfcl  18255  prfcl  18260  evlfcl  18279  curf1cl  18285  curfcl  18289  hofcl  18316  latjlej12  18512  latmlem12  18528  latj4  18546  latj4rot  18547  symgsssg  19538  symgfisg  19539  odcong  19620  cmn4  19872  ablsub4  19881  abladdsub4  19882  lsm4  19931  abvdom  20914  abvtrivd  20916  orngmul  20949  lspsolvlem  21247  lbsextlem2  21264  lidlsubcl  21330  frlmbas3  21907  matinvgcell  22573  matmulcell  22583  ma1repveval  22709  mdetunilem3  22752  mdetuni0  22759  mdetmul  22761  hausflimlem  24117  psmetlecl  24453  xmetlecl  24484  prdsxmetlem  24506  xblcntrps  24548  xblcntr  24549  bndth  25098  cph2ass  25353  iscau3  25418  dvres2  26052  coemullem  26388  vieta1  26454  aalioulem4  26479  cxpcn3lem  26893  angcan  26948  divsqrtsumlem  27125  dchrmusumlema  27638  dchrvmasumlema  27645  dchrisum0lema  27659  logdivsum  27678  padicabv  27775  cofcut1  28094  cofcut2  28096  divmulsw  28367  precsexlem8  28388  precsexlem9  28389  bdayfinbndlem1  28641  ax5seglem3  29262  ax5seglem6  29265  axpasch  29272  axeuclid  29294  axcontlem4  29298  axcontlem8  29302  trlsonistrl  30037  pthonispth  30076  spthonisspth  30080  wspthneq1eq2  30190  frgr2wwlkeqm  30663  adjlnop  32419  xreceu  33222  rhmdvd  33625  measvunilem  34583  measvuni  34585  bnj1128  35359  umgr2cycl  35614  satfv1fvfmla1  35896  cgrcomim  36462  cgrcoml  36469  cgrcomr  36470  cgrdegen  36477  segconeu  36484  btwnintr  36492  btwnexch3  36493  btwnouttr2  36495  btwnouttr  36497  btwnexch  36498  ifscgr  36517  lineext  36549  linecgr  36554  lineid  36556  idinside  36557  btwnconn1lem3  36562  btwnconn1lem4  36563  btwnconn1lem14  36573  btwnconn2  36575  btwnconn3  36576  midofsegid  36577  btwnoutside  36598  outsideoftr  36602  lineunray  36620  lineelsb2  36621  itg2addnclem  38303  cnres2  38395  heibor  38453  lsmcv2  39784  lcvat  39785  lcvexchlem4  39792  lcvexchlem5  39793  lfladd  39821  lflsub  39822  lflmul  39823  lshpkrlem4  39868  latm4  39988  omlmod1i2N  40015  cvlsupr7  40103  cvlsupr8  40104  hlatj4  40129  hlrelat3  40167  cvrval3  40168  atcvrj1  40186  atlelt  40193  2atlt  40194  2atjm  40200  3noncolr2  40204  athgt  40211  3dimlem2  40214  3dimlem4OLDN  40220  1cvratex  40228  ps-1  40232  ps-2  40233  hlatexch3N  40235  llnle  40273  atcvrlln2  40274  atcvrlln  40275  lplni2  40292  lplnle  40295  lplnnle2at  40296  lplnnlelln  40298  llncvrlpln2  40312  2llnmeqat  40326  lvolnle3at  40337  lvolnlelln  40339  4atlem0ae  40349  lneq2at  40533  lnjatN  40535  lncvrat  40537  2lnat  40539  elpaddri  40557  paddasslem2  40576  padd4N  40595  hlmod1i  40611  llnexchb2  40624  dalawlem2  40627  pclfinN  40655  pexmidlem4N  40728  pl42lem1N  40734  lhp2lt  40756  lhpexle1  40763  lhpexle2lem  40764  lhpj1  40777  lhpmcvr5N  40782  lhp2at0  40787  lhp2at0nle  40790  lhple  40797  lhpat  40798  lhpat4N  40799  4atexlemnslpq  40811  4atexlem7  40830  ltrn11  40881  ltrnle  40884  ltrnm  40886  ltrnj  40887  ltrncvr  40888  ltrnel  40894  ltrncnvel  40897  ltrncnv  40901  trlat  40924  trl0  40925  trlnidat  40928  trlnid  40934  ltrnatlw  40938  trlne  40940  trlval4  40943  cdlemc5  40950  cdlemd2  40954  cdlemd7  40959  cdlemd8  40960  cdlemd9  40961  cdleme0c  40968  cdleme0e  40972  cdleme0fN  40973  cdleme3g  40989  cdleme3h  40990  cdleme5  40995  cdleme11c  41016  cdleme11h  41021  cdleme11j  41022  cdleme11k  41023  cdleme0nex  41045  cdleme18a  41046  cdleme22gb  41049  cdleme20zN  41056  cdleme20c  41066  cdleme20k  41074  cdleme21a  41080  cdleme21b  41081  cdleme21c  41082  cdleme21ct  41084  cdleme21h  41089  cdleme22d  41098  cdleme22f  41101  cdleme26ee  41115  cdleme30a  41133  cdlemefs45eN  41186  cdleme36a  41215  cdleme36m  41216  cdleme39a  41220  cdleme42b  41233  cdleme43dN  41247  cdlemeg47rv2  41265  cdlemeg46sfg  41275  cdlemeg46rjgN  41277  cdlemeg46rgv  41283  cdlemeg46req  41284  cdlemeg46gfv  41285  cdleme48d  41290  cdleme50ltrn  41312  cdlemf1  41316  cdlemf  41318  cdlemg2dN  41345  cdlemg2fvlem  41349  cdlemg2l  41358  cdlemg7fvbwN  41362  cdlemg7aN  41380  cdlemg10c  41394  cdlemg17a  41416  cdlemg17dALTN  41419  cdlemg18a  41433  cdlemg18b  41434  cdlemg31b0a  41450  cdlemg31a  41452  cdlemg31b  41453  ltrnco  41474  cdlemg48  41492  tgrpov  41503  tendoco2  41523  tendoplco2  41534  cdlemh1  41570  cdlemk1  41586  cdlemk26b-3  41660  cdlemk27-3  41662  cdlemk28-3  41663  cdlemk34  41665  cdlemkfid1N  41676  cdlemkid3N  41688  cdlemkid4  41689  cdlemk35s-id  41693  cdlemk39s-id  41695  cdlemk51  41708  tendospcanN  41778  cdlemm10N  41873  dicvaddcl  41945  dicvscacl  41946  cdlemn6  41957  dihvalcq2  42002  dihord6b  42015  dihord5apre  42017  dihglbcpreN  42055  dihjatc1  42066  dihmeetlem20N  42081  dih1dimatlem0  42083  dihglblem6  42095  dochexmidlem4  42218  mapdpglem32  42460  mapdh8ad  42534  mapdh9aOLDN  42545  hdmap11lem2  42597  hdmap14lem6  42628  frlmfzowrdb  43259  mzpmfp  43461  mzpsubst  43462  pellex  43545  pellfundex  43596  pellfund14gap  43597  qirropth  43618  rmxypos  43657  congmul  43677  congsub  43680  mzpcong  43682  coprmdvdsb  43695  jm2.15nn0  43713  jm2.16nn0  43714  rpnnen3lem  43741  idomsubgmo  43903  relexp01min  44422  mullimc  46315  islptre  46318  mullimcf  46322  addlimc  46345  0ellimcdiv  46346  limsupre3lem  46429  limsupre3uzlem  46432  fourierdlem48  46851  fourierdlem80  46883  opnvonmbllem2  47330  ovolval5lem3  47351  ovnovollem3  47355  difltmodne  48068  isubgr3stgrlem1  48714  grlimedgclnbgr  48743  mapprop  49109  lincfsuppcl  49176  lindslinindimp2lem3  49223  itsclc0lem1  49519  itsclc0lem2  49520  itschlc0yqe  49523  itsclc0xyqsolr  49532  swapffunc  50043  fucofunc  50120  fucoppc  50171