Theorem simpl3 1029

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

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

Proof of Theorem simpl3

Step	Hyp	Ref	Expression
1		simp3 1026	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	adantr 276	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  simpll3  1065  simprl3  1071  simp1l3  1119  simp2l3  1125  simp3l3  1131  3anandirs  1385  ifnetruedc  3668  frirrg  4473  fcofo  5959  acexmid  6051  rdgon  6619  oawordi  6704  nnmord  6752  nnmword  6753  1dom1el  7062  mapunen  7106  fidifsnen  7127  dif1en  7138  ac6sfi  7157  fissfi  7218  difinfsn  7393  2omotaplemap  7573  enq0tr  7751  distrlem4prl  7901  distrlem4pru  7902  ltaprg  7936  lelttr  8364  ltletr  8365  readdcan  8415  addcan  8455  addcan2  8456  ltadd2  8695  divmulassap  8971  xrlelttr  10142  xrltletr  10143  xaddass  10205  xleadd1a  10209  xlesubadd  10219  icoshftf1o  10327  lincmble  10340  difelfzle  10472  fzo1fzo0n0  10526  modqmuladdim  10733  modqmuladdnn0  10734  modqm1p1mod0  10741  q2submod  10751  modifeq2int  10752  modqaddmulmod  10757  seq1g  10829  seqp1g  10832  ltexp2a  10957  exple1  10961  expnlbnd2  11031  nn0ltexp2  11075  nn0leexp2  11076  mulsubdivbinom2ap  11077  expcan  11082  fiprsshashgt1  11186  hashtpgim  11221  hashtpg  11223  fun2dmnop0  11226  ccatass  11300  fzowrddc  11343  swrdclg  11346  ccatopth  11412  pfxccatin12lem2a  11423  pfxccat3  11430  maxleastb  11903  maxltsup  11907  xrltmaxsup  11946  xrmaxltsup  11947  xrmaxaddlem  11949  xrmaxadd  11950  addcn2  11999  mulcn2  12001  isumz  12079  dvdsmodexp  12485  modmulconst  12513  dvdsmod  12552  divalglemex  12612  divalg  12614  gcdass  12715  rplpwr  12727  rppwr  12728  nnwodc  12736  uzwodc  12737  rpmulgcd2  12796  rpdvds  12800  rpexp  12854  znege1  12879  prmdiveq  12937  hashgcdlem  12939  coprimeprodsq  12959  coprimeprodsq2  12960  pythagtriplem3  12969  pcdvdsb  13022  pcgcd1  13030  dvdsprmpweq  13037  pcbc  13053  ctinf  13198  nninfdc  13221  isnsgrp  13636  issubmnd  13672  mulgnn0p1  13867  mulgnnsubcl  13868  mulgneg  13874  mulgdirlem  13887  nmzsubg  13944  ghmmulg  13990  ring1eq0  14209  rmodislmod  14516  lspss  14564  2idlcpblrng  14688  neiint  15027  topssnei  15044  cnptopco  15104  cnrest2  15118  cnptoprest  15121  upxp  15154  bldisj  15283  blgt0  15284  bl2in  15285  blss2ps  15288  blss2  15289  xblm  15299  blssps  15309  blss  15310  bdmopn  15386  metcnp2  15395  txmetcnp  15400  cncfmptc  15478  dvcnp2cntop  15581  dvcn  15582  ply1term  15625  dvply1  15647  logdivlti  15763  ltexp2  15823  pellexlem2  15863  lgsfvalg  15895  lgsneg  15914  lgsmod  15916  lgsdilem  15917  lgsdirprm  15924  lgsdir  15925  lgsdi  15927  lgsne0  15928  gfsumsn  16884