Theorem simp3l 1220

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

Assertion

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

Proof of Theorem simp3l

Step	Hyp	Ref	Expression
1		simpl 488	. 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:  simp13l  1307  simp23l  1313  simp33l  1319  tfisi  7897  fpr3g  8334  tfrlem5  8418  omeulem1  8621  omeulem2  8622  uniinqs  8849  elfiun  9452  tcrank  9931  isfin2-2  10427  konigthlem  10683  gruen  10927  addlid  11523  mulcan  11983  mulcan2  11984  divass  12022  divdir  12029  muldivdir  12039  subdivcomb1  12042  subdivcomb2  12043  divcan5  12049  ltmul1  12197  ltdiv1  12211  ltmuldiv  12220  lediv2  12237  xaddass2  13410  xlt2add  13420  xmulasslem3  13446  xadddi2  13457  expaddz  14279  expmulz  14281  muldivbinom2  14437  resqrtcl  15452  o1add  15813  o1mul  15814  o1sub  15815  dvdsadd2b  16508  dvdsgcd  16749  rpexp12i  16932  pythagtriplem3  17028  pcpremul  17053  pceu  17056  pcqmul  17063  pcqdiv  17067  setsstruct  17386  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  psgnunilem4  19744  odcong  19796  cmn4  20048  ablsub4  20057  abladdsub4  20058  lsm4  20107  abvdom  21120  abvres  21121  abvtrivd  21122  orngmul  21155  lspsolvlem  21453  lbsextlem2  21470  lidlsubcl  21536  frlmbas3  22115  matmulcell  22793  marrepeval  22911  ma1repveval  22919  submaeval  22930  mdetunilem3  22962  mdetuni0  22969  mdetmul  22971  minmar1eval  22997  nllyrest  23838  hausflimlem  24331  tsmsxp  24507  psmetlecl  24667  xmetlecl  24698  prdsxmetlem  24720  ngpocelbl  25056  bndth  25312  cph2ass  25567  iscau3  25632  dvres2  26265  coemullem  26602  vieta1  26668  aalioulem4  26695  cxpcn3lem  27108  angcan  27163  dchrvmasumlema  27860  logdivsum  27893  abvcxp  27975  padicabv  27990  flt4lem5  28013  nosupbnd1lem4  28101  nosupbnd1lem5  28102  noinfbnd1lem4  28116  cofcut1  28339  cofcut2  28341  divmulsw  28612  precsexlem8  28633  precsexlem9  28634  bdayfinbndlem1  28886  ax5seglem3  29542  ax5seglem6  29545  axpasch  29552  axeuclid  29574  axcontlem4  29578  axcontlem8  29582  wlkl1loop  30251  trlsonwlkon  30325  pthontrlon  30366  wspthsswwlknon  30543  umgr2cycllem  30779  umgr2cycl  30780  frgr2wwlkeqm  30965  adjlnop  32721  xreceu  33561  rhmdvd  33969  measvunilem  34928  measvunilem0  34929  measres  34938  bnj1128  35703  satfv1fvfmla1  36368  cgrcomim  36945  cgrcoml  36952  cgrcomr  36953  cgrdegen  36960  segconeu  36967  btwnintr  36975  btwnexch3  36976  btwnouttr2  36978  btwnouttr  36980  btwnexch  36981  trisegint  36984  lineext  37032  linecgr  37037  lineid  37039  idinside  37040  btwnconn1lem3  37045  btwnconn1lem4  37046  btwnconn1lem7  37049  btwnconn1lem14  37056  btwnconn2  37058  midofsegid  37060  btwnoutside  37081  outsideoftr  37085  lineunray  37103  lineelsb2  37104  cnres2  38900  heibor  38958  lsmcv2  40289  lcvat  40290  lcvexchlem4  40297  lcvexchlem5  40298  lfladd  40326  lflsub  40327  lflmul  40328  lshpkrlem4  40373  latm4  40493  omlmod1i2N  40520  cvlatexch3  40598  cvlsupr7  40608  hlatj4  40634  hlrelat3  40672  cvrval3  40673  atcvrj1  40691  atlelt  40698  2atlt  40699  2atjm  40705  3noncolr2  40709  athgt  40716  3dimlem2  40719  3dimlem4  40724  3dimlem4OLDN  40725  3dim3  40729  1cvratex  40733  ps-1  40737  ps-2  40738  hlatexch3N  40740  llnle  40778  atcvrlln2  40779  atcvrlln  40780  lplni2  40797  lplnle  40800  lplnnle2at  40801  llncvrlpln2  40817  lplnexllnN  40824  2llnmeqat  40831  lvolnle3at  40842  4atlem0ae  40854  lplncvrlvol2  40875  lnjatN  41040  lncvrat  41042  cdlemblem  41053  elpaddri  41062  paddasslem2  41081  paddasslem16  41095  padd4N  41100  hlmod1i  41116  dalawlem2  41132  pclfinN  41160  pexmidlem4N  41233  pl42lem1N  41239  lhp2lt  41261  lhpexle1  41268  lhpexle2lem  41269  lhpj1  41282  lhpmcvr5N  41287  lhp2at0  41292  lhp2atnle  41293  lhp2at0nle  41295  lhple  41302  lhpat  41303  lhpat4N  41304  4atexlempnq  41315  4atexlem7  41335  4atex  41336  ltrn11  41386  ltrnle  41389  ltrnm  41391  ltrnj  41392  ltrncvr  41393  ltrnel  41399  ltrncnvel  41402  ltrncnv  41406  trlval2  41423  trlcnv  41425  trljat1  41426  trljat2  41427  trlat  41429  trl0  41430  trlnidat  41433  trlnid  41439  cdlemc1  41451  cdlemc2  41452  cdlemc5  41455  cdlemd2  41459  cdlemd7  41464  cdlemd8  41465  cdlemd9  41466  cdleme0e  41477  cdleme3g  41494  cdleme3h  41495  cdleme3  41497  cdleme5  41500  cdleme10  41514  cdleme11a  41520  cdleme11c  41521  cdleme11h  41526  cdleme11j  41527  cdleme0nex  41550  cdleme18a  41551  cdleme18b  41552  cdleme22gb  41554  cdleme20zN  41561  cdleme20c  41571  cdleme20k  41579  cdleme21a  41585  cdleme21b  41586  cdleme21c  41587  cdleme21h  41594  cdleme22b  41601  cdleme22d  41603  cdleme22f  41606  cdleme25a  41613  cdleme25c  41615  cdleme25dN  41616  cdleme26ee  41620  cdleme30a  41638  cdlemefr29bpre0N  41666  cdlemefr29clN  41667  cdlemefr32fvaN  41669  cdlemefr32fva1  41670  cdlemefs29bpre0N  41676  cdlemefs29bpre1N  41677  cdlemefs29cpre1N  41678  cdlemefs29clN  41679  cdleme43fsv1snlem  41680  cdlemefs32fvaN  41682  cdlemefs32fva1  41683  cdlemefs31fv1  41684  cdleme36a  41720  cdleme39a  41725  cdleme42a  41731  cdleme42c  41732  cdleme17d3  41756  cdleme48fv  41759  cdleme48bw  41762  cdleme48b  41763  cdlemeg46rgv  41788  cdlemeg46req  41789  cdlemeg46gfv  41790  cdleme48d  41795  cdleme50trn2a  41810  cdleme50trn2  41811  cdleme50ltrn  41817  cdlemf1  41821  cdlemf  41823  trlord  41829  cdlemg2dN  41850  cdlemg2fvlem  41854  cdlemg2l  41863  cdlemg7fvbwN  41867  cdlemg7aN  41885  cdlemg10bALTN  41896  cdlemg10c  41899  cdlemg17a  41921  cdlemg17dALTN  41924  cdlemg31b0a  41955  cdlemg31a  41957  cdlemg31b  41958  cdlemg34  41972  cdlemg36  41974  ltrnco  41979  trlcoabs2N  41982  trlcolem  41986  cdlemg48  41997  tgrpov  42008  tendoco2  42028  tendoplco2  42039  cdlemh1  42075  cdlemi1  42078  cdlemi2  42079  cdlemj3  42083  tendoid0  42085  cdlemk1  42091  cdlemk2  42092  cdlemk4  42094  cdlemk8  42098  cdlemk9  42099  cdlemk9bN  42100  cdlemk10  42103  cdlemk26b-3  42165  cdlemk26-3  42166  cdlemk28-3  42168  cdlemk37  42174  cdlemk39  42176  cdlemkfid1N  42181  cdlemkid1  42182  cdlemky  42186  cdlemkyu  42187  cdlemk19ylem  42190  cdlemk19xlem  42202  cdlemk11t  42206  cdlemk51  42213  cdlemkyyN  42222  cdleml6  42241  cdleml7  42242  cdleml8  42243  cdleml9  42244  erngdvlem4  42251  erngdvlem4-rN  42259  tendospcanN  42283  dia11N  42308  cdlemm10N  42378  dib11N  42420  dicvaddcl  42450  dicvscacl  42451  cdlemn6  42462  dihvalcq2  42507  dihopelvalcpre  42508  dihord6b  42520  dihord5apre  42522  dihmeetlem1N  42550  dihmeetlem2N  42559  dihglbcpreN  42560  dihjatc1  42571  dihmeetlem20N  42586  dih1dimatlem0  42588  dihatlat  42594  dihglblem6  42600  dochexmidlem4  42723  mapdpglem32  42965  mapdh8ad  43039  mapdh9aOLDN  43050  hdmap11lem2  43102  hdmap14lem6  43133  frlmfzowrdb  43775  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  limccog  46847  mullimcf  46850  addlimc  46873  0ellimcdiv  46874  limsupre3lem  46957  stoweidlem57  47282  fourierdlem48  47379  fourierdlem80  47411  fourierdlem113  47444  ovncvrrp  47789  opnvonmbllem2  47858  ovolval5lem3  47879  ovnovollem3  47883  grlimedgclnbgr  49308  itsclc0lem1  50083  itsclc0lem2  50084  itschlc0yqe  50087  itscnhlc0xyqsol  50092  itschlc0xyqsol1  50093  swapffunc  50619  fucofunc  50696  fucoppc  50760  parmapfunc2  50989  parmapfunc  50990