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  7386  tfisi  7897  tfrlem5  8418  omeulem1  8621  omeulem2  8622  elfiun  9452  isfin2-2  10427  addlid  11523  mulcan  11983  mulcan2  11984  divass  12022  divdir  12029  ltdiv1  12211  ltmuldiv  12220  lediv2  12237  xaddass2  13410  xlt2add  13420  expaddz  14279  expmulz  14281  resqrex  15449  resqrtcl  15452  o1add  15813  o1mul  15814  o1sub  15815  dvdsgcd  16749  rpexp12i  16932  pythagtriplem4  17029  pythagtriplem11  17035  pythagtriplem13  17037  pcpremul  17053  pceu  17056  pcqmul  17063  pcqdiv  17067  f1ocpbllem  17728  funcoppc  18082  funcres  18103  catcisolem  18317  1stfcl  18403  2ndfcl  18404  prfcl  18409  evlfcl  18428  curf1cl  18434  curfcl  18438  hofcl  18465  latjlej12  18661  latmlem12  18677  latj4  18695  latj4rot  18696  symgsssg  19714  symgfisg  19715  odcong  19796  cmn4  20048  ablsub4  20057  abladdsub4  20058  lsm4  20107  abvdom  21120  abvtrivd  21122  orngmul  21155  lspsolvlem  21453  lbsextlem2  21470  lidlsubcl  21536  frlmbas3  22115  matinvgcell  22783  matmulcell  22793  ma1repveval  22919  mdetunilem3  22962  mdetuni0  22969  mdetmul  22971  hausflimlem  24331  psmetlecl  24667  xmetlecl  24698  prdsxmetlem  24720  xblcntrps  24762  xblcntr  24763  bndth  25312  cph2ass  25567  iscau3  25632  dvres2  26265  coemullem  26602  vieta1  26668  aalioulem4  26695  cxpcn3lem  27108  angcan  27163  divsqrtsumlem  27340  dchrmusumlema  27853  dchrvmasumlema  27860  dchrisum0lema  27874  logdivsum  27893  padicabv  27990  cofcut1  28339  cofcut2  28341  divmulsw  28612  precsexlem8  28633  precsexlem9  28634  bdayfinbndlem1  28886  ax5seglem3  29542  ax5seglem6  29545  axpasch  29552  axeuclid  29574  axcontlem4  29578  axcontlem8  29582  trlsonistrl  30324  pthonispth  30365  spthonisspth  30369  wspthneq1eq2  30482  umgr2cycllem  30779  umgr2cycl  30780  frgr2wwlkeqm  30965  adjlnop  32721  xreceu  33561  rhmdvd  33969  measvunilem  34928  measvuni  34930  bnj1128  35703  satfv1fvfmla1  36368  cgrcomim  36945  cgrcoml  36952  cgrcomr  36953  cgrdegen  36960  segconeu  36967  btwnintr  36975  btwnexch3  36976  btwnouttr2  36978  btwnouttr  36980  btwnexch  36981  ifscgr  37000  lineext  37032  linecgr  37037  lineid  37039  idinside  37040  btwnconn1lem3  37045  btwnconn1lem4  37046  btwnconn1lem14  37056  btwnconn2  37058  btwnconn3  37059  midofsegid  37060  btwnoutside  37081  outsideoftr  37085  lineunray  37103  lineelsb2  37104  itg2addnclem  38794  cnres2  38900  heibor  38958  lsmcv2  40289  lcvat  40290  lcvexchlem4  40297  lcvexchlem5  40298  lfladd  40326  lflsub  40327  lflmul  40328  lshpkrlem4  40373  latm4  40493  omlmod1i2N  40520  cvlsupr7  40608  cvlsupr8  40609  hlatj4  40634  hlrelat3  40672  cvrval3  40673  atcvrj1  40691  atlelt  40698  2atlt  40699  2atjm  40705  3noncolr2  40709  athgt  40716  3dimlem2  40719  3dimlem4OLDN  40725  1cvratex  40733  ps-1  40737  ps-2  40738  hlatexch3N  40740  llnle  40778  atcvrlln2  40779  atcvrlln  40780  lplni2  40797  lplnle  40800  lplnnle2at  40801  lplnnlelln  40803  llncvrlpln2  40817  2llnmeqat  40831  lvolnle3at  40842  lvolnlelln  40844  4atlem0ae  40854  lneq2at  41038  lnjatN  41040  lncvrat  41042  2lnat  41044  elpaddri  41062  paddasslem2  41081  padd4N  41100  hlmod1i  41116  llnexchb2  41129  dalawlem2  41132  pclfinN  41160  pexmidlem4N  41233  pl42lem1N  41239  lhp2lt  41261  lhpexle1  41268  lhpexle2lem  41269  lhpj1  41282  lhpmcvr5N  41287  lhp2at0  41292  lhp2at0nle  41295  lhple  41302  lhpat  41303  lhpat4N  41304  4atexlemnslpq  41316  4atexlem7  41335  ltrn11  41386  ltrnle  41389  ltrnm  41391  ltrnj  41392  ltrncvr  41393  ltrnel  41399  ltrncnvel  41402  ltrncnv  41406  trlat  41429  trl0  41430  trlnidat  41433  trlnid  41439  ltrnatlw  41443  trlne  41445  trlval4  41448  cdlemc5  41455  cdlemd2  41459  cdlemd7  41464  cdlemd8  41465  cdlemd9  41466  cdleme0c  41473  cdleme0e  41477  cdleme0fN  41478  cdleme3g  41494  cdleme3h  41495  cdleme5  41500  cdleme11c  41521  cdleme11h  41526  cdleme11j  41527  cdleme11k  41528  cdleme0nex  41550  cdleme18a  41551  cdleme22gb  41554  cdleme20zN  41561  cdleme20c  41571  cdleme20k  41579  cdleme21a  41585  cdleme21b  41586  cdleme21c  41587  cdleme21ct  41589  cdleme21h  41594  cdleme22d  41603  cdleme22f  41606  cdleme26ee  41620  cdleme30a  41638  cdlemefs45eN  41691  cdleme36a  41720  cdleme36m  41721  cdleme39a  41725  cdleme42b  41738  cdleme43dN  41752  cdlemeg47rv2  41770  cdlemeg46sfg  41780  cdlemeg46rjgN  41782  cdlemeg46rgv  41788  cdlemeg46req  41789  cdlemeg46gfv  41790  cdleme48d  41795  cdleme50ltrn  41817  cdlemf1  41821  cdlemf  41823  cdlemg2dN  41850  cdlemg2fvlem  41854  cdlemg2l  41863  cdlemg7fvbwN  41867  cdlemg7aN  41885  cdlemg10c  41899  cdlemg17a  41921  cdlemg17dALTN  41924  cdlemg18a  41938  cdlemg18b  41939  cdlemg31b0a  41955  cdlemg31a  41957  cdlemg31b  41958  ltrnco  41979  cdlemg48  41997  tgrpov  42008  tendoco2  42028  tendoplco2  42039  cdlemh1  42075  cdlemk1  42091  cdlemk26b-3  42165  cdlemk27-3  42167  cdlemk28-3  42168  cdlemk34  42170  cdlemkfid1N  42181  cdlemkid3N  42193  cdlemkid4  42194  cdlemk35s-id  42198  cdlemk39s-id  42200  cdlemk51  42213  tendospcanN  42283  cdlemm10N  42378  dicvaddcl  42450  dicvscacl  42451  cdlemn6  42462  dihvalcq2  42507  dihord6b  42520  dihord5apre  42522  dihglbcpreN  42560  dihjatc1  42571  dihmeetlem20N  42586  dih1dimatlem0  42588  dihglblem6  42600  dochexmidlem4  42723  mapdpglem32  42965  mapdh8ad  43039  mapdh9aOLDN  43050  hdmap11lem2  43102  hdmap14lem6  43133  frlmfzowrdb  43775  mzpmfp  43962  mzpsubst  43963  pellex  44046  pellfundex  44097  pellfund14gap  44098  qirropth  44119  rmxypos  44158  congmul  44178  congsub  44181  mzpcong  44183  coprmdvdsb  44196  jm2.15nn0  44214  jm2.16nn0  44215  rpnnen3lem  44242  idomsubgmo  44398  relexp01min  44916  mullimc  46843  islptre  46846  mullimcf  46850  addlimc  46873  0ellimcdiv  46874  limsupre3lem  46957  limsupre3uzlem  46960  fourierdlem48  47379  fourierdlem80  47411  opnvonmbllem2  47858  ovolval5lem3  47879  ovnovollem3  47883  difltmodne  48633  isubgr3stgrlem1  49279  grlimedgclnbgr  49308  mapprop  49673  lincfsuppcl  49740  lindslinindimp2lem3  49787  itsclc0lem1  50083  itsclc0lem2  50084  itschlc0yqe  50087  itsclc0xyqsolr  50096  swapffunc  50619  fucofunc  50696  fucoppc  50760  parmapfunc2  50989  parmapfunc  50990