Theorem simp3r 1209

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp13r  1296  simp23r  1302  simp33r  1308  f1oiso2  7303  tfisi  7806  tfrlem5  8316  omeulem1  8514  omeulem2  8515  elfiun  9340  isfin2-2  10239  addlid  11327  mulcan  11785  mulcan2  11786  divass  11825  divdir  11832  div11OLD  11836  ltdiv1  12018  ltmuldiv  12027  lediv2  12044  xaddass2  13200  xlt2add  13210  expaddz  14066  expmulz  14068  resqrex  15210  resqrtcl  15213  o1add  15574  o1mul  15575  o1sub  15576  dvdsgcd  16511  rpexp12i  16692  pythagtriplem4  16788  pythagtriplem11  16794  pythagtriplem13  16796  pcpremul  16812  pceu  16815  pcqmul  16822  pcqdiv  16826  f1ocpbllem  17486  funcoppc  17840  funcres  17861  catcisolem  18075  1stfcl  18161  2ndfcl  18162  prfcl  18167  evlfcl  18186  curf1cl  18192  curfcl  18196  hofcl  18223  latjlej12  18419  latmlem12  18435  latj4  18453  latj4rot  18454  symgsssg  19440  symgfisg  19441  odcong  19522  cmn4  19774  ablsub4  19783  abladdsub4  19784  lsm4  19833  abvdom  20809  abvtrivd  20811  orngmul  20844  lspsolvlem  21142  lbsextlem2  21159  lidlsubcl  21224  frlmbas3  21758  matinvgcell  22425  matmulcell  22435  ma1repveval  22561  mdetunilem3  22604  mdetuni0  22611  mdetmul  22613  hausflimlem  23969  psmetlecl  24305  xmetlecl  24336  prdsxmetlem  24358  xblcntrps  24400  xblcntr  24401  bndth  24950  cph2ass  25205  iscau3  25270  dvres2  25904  coemullem  26240  vieta1  26303  aalioulem4  26326  cxpcn3lem  26736  angcan  26791  divsqrtsumlem  26968  dchrmusumlema  27481  dchrvmasumlema  27488  dchrisum0lema  27502  logdivsum  27521  padicabv  27618  cofcut1  27937  cofcut2  27939  divmulsw  28210  precsexlem8  28231  precsexlem9  28232  bdayfinbndlem1  28484  ax5seglem3  29025  ax5seglem6  29028  axpasch  29035  axeuclid  29057  axcontlem4  29061  axcontlem8  29065  trlsonistrl  29800  pthonispth  29839  spthonisspth  29843  wspthneq1eq2  29953  frgr2wwlkeqm  30426  adjlnop  32182  xreceu  33007  rhmdvd  33414  measvunilem  34403  measvuni  34405  bnj1128  35179  umgr2cycl  35376  satfv1fvfmla1  35658  cgrcomim  36224  cgrcoml  36231  cgrcomr  36232  cgrdegen  36239  segconeu  36246  btwnintr  36254  btwnexch3  36255  btwnouttr2  36257  btwnouttr  36259  btwnexch  36260  ifscgr  36279  lineext  36311  linecgr  36316  lineid  36318  idinside  36319  btwnconn1lem3  36324  btwnconn1lem4  36325  btwnconn1lem14  36335  btwnconn2  36337  btwnconn3  36338  midofsegid  36339  btwnoutside  36360  outsideoftr  36364  lineunray  36382  lineelsb2  36383  itg2addnclem  38045  cnres2  38137  heibor  38195  lsmcv2  39528  lcvat  39529  lcvexchlem4  39536  lcvexchlem5  39537  lfladd  39565  lflsub  39566  lflmul  39567  lshpkrlem4  39612  latm4  39732  omlmod1i2N  39759  cvlsupr7  39847  cvlsupr8  39848  hlatj4  39873  hlrelat3  39911  cvrval3  39912  atcvrj1  39930  atlelt  39937  2atlt  39938  2atjm  39944  3noncolr2  39948  athgt  39955  3dimlem2  39958  3dimlem4OLDN  39964  1cvratex  39972  ps-1  39976  ps-2  39977  hlatexch3N  39979  llnle  40017  atcvrlln2  40018  atcvrlln  40019  lplni2  40036  lplnle  40039  lplnnle2at  40040  lplnnlelln  40042  llncvrlpln2  40056  2llnmeqat  40070  lvolnle3at  40081  lvolnlelln  40083  4atlem0ae  40093  lneq2at  40277  lnjatN  40279  lncvrat  40281  2lnat  40283  elpaddri  40301  paddasslem2  40320  padd4N  40339  hlmod1i  40355  llnexchb2  40368  dalawlem2  40371  pclfinN  40399  pexmidlem4N  40472  pl42lem1N  40478  lhp2lt  40500  lhpexle1  40507  lhpexle2lem  40508  lhpj1  40521  lhpmcvr5N  40526  lhp2at0  40531  lhp2at0nle  40534  lhple  40541  lhpat  40542  lhpat4N  40543  4atexlemnslpq  40555  4atexlem7  40574  ltrn11  40625  ltrnle  40628  ltrnm  40630  ltrnj  40631  ltrncvr  40632  ltrnel  40638  ltrncnvel  40641  ltrncnv  40645  trlat  40668  trl0  40669  trlnidat  40672  trlnid  40678  ltrnatlw  40682  trlne  40684  trlval4  40687  cdlemc5  40694  cdlemd2  40698  cdlemd7  40703  cdlemd8  40704  cdlemd9  40705  cdleme0c  40712  cdleme0e  40716  cdleme0fN  40717  cdleme3g  40733  cdleme3h  40734  cdleme5  40739  cdleme11c  40760  cdleme11h  40765  cdleme11j  40766  cdleme11k  40767  cdleme0nex  40789  cdleme18a  40790  cdleme22gb  40793  cdleme20zN  40800  cdleme20c  40810  cdleme20k  40818  cdleme21a  40824  cdleme21b  40825  cdleme21c  40826  cdleme21ct  40828  cdleme21h  40833  cdleme22d  40842  cdleme22f  40845  cdleme26ee  40859  cdleme30a  40877  cdlemefs45eN  40930  cdleme36a  40959  cdleme36m  40960  cdleme39a  40964  cdleme42b  40977  cdleme43dN  40991  cdlemeg47rv2  41009  cdlemeg46sfg  41019  cdlemeg46rjgN  41021  cdlemeg46rgv  41027  cdlemeg46req  41028  cdlemeg46gfv  41029  cdleme48d  41034  cdleme50ltrn  41056  cdlemf1  41060  cdlemf  41062  cdlemg2dN  41089  cdlemg2fvlem  41093  cdlemg2l  41102  cdlemg7fvbwN  41106  cdlemg7aN  41124  cdlemg10c  41138  cdlemg17a  41160  cdlemg17dALTN  41163  cdlemg18a  41177  cdlemg18b  41178  cdlemg31b0a  41194  cdlemg31a  41196  cdlemg31b  41197  ltrnco  41218  cdlemg48  41236  tgrpov  41247  tendoco2  41267  tendoplco2  41278  cdlemh1  41314  cdlemk1  41330  cdlemk26b-3  41404  cdlemk27-3  41406  cdlemk28-3  41407  cdlemk34  41409  cdlemkfid1N  41420  cdlemkid3N  41432  cdlemkid4  41433  cdlemk35s-id  41437  cdlemk39s-id  41439  cdlemk51  41452  tendospcanN  41522  cdlemm10N  41617  dicvaddcl  41689  dicvscacl  41690  cdlemn6  41701  dihvalcq2  41746  dihord6b  41759  dihord5apre  41761  dihglbcpreN  41799  dihjatc1  41810  dihmeetlem20N  41825  dih1dimatlem0  41827  dihglblem6  41839  dochexmidlem4  41962  mapdpglem32  42204  mapdh8ad  42278  mapdh9aOLDN  42289  hdmap11lem2  42341  hdmap14lem6  42372  frlmfzowrdb  43001  mzpmfp  43203  mzpsubst  43204  pellex  43287  pellfundex  43338  pellfund14gap  43339  qirropth  43360  rmxypos  43399  congmul  43419  congsub  43422  mzpcong  43424  coprmdvdsb  43437  jm2.15nn0  43455  jm2.16nn0  43456  rpnnen3lem  43483  idomsubgmo  43645  relexp01min  44164  mullimc  46068  islptre  46071  mullimcf  46075  addlimc  46098  0ellimcdiv  46099  limsupre3lem  46182  limsupre3uzlem  46185  fourierdlem48  46604  fourierdlem80  46636  opnvonmbllem2  47083  ovolval5lem3  47104  ovnovollem3  47108  difltmodne  47818  isubgr3stgrlem1  48464  grlimedgclnbgr  48493  mapprop  48844  lincfsuppcl  48911  lindslinindimp2lem3  48958  itsclc0lem1  49254  itsclc0lem2  49255  itschlc0yqe  49258  itsclc0xyqsolr  49267  swapffunc  49779  fucofunc  49856  fucoppc  49907