Theorem simpl3 1026

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

Assertion

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

Proof of Theorem simpl3

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

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

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 1004

This theorem is referenced by:  simpll3  1062  simprl3  1068  simp1l3  1116  simp2l3  1122  simp3l3  1128  3anandirs  1382  ifnetruedc  3646  frirrg  4441  fcofo  5914  acexmid  6006  rdgon  6538  oawordi  6623  nnmord  6671  nnmword  6672  fidifsnen  7040  dif1en  7049  ac6sfi  7068  difinfsn  7275  2omotaplemap  7451  enq0tr  7629  distrlem4prl  7779  distrlem4pru  7780  ltaprg  7814  lelttr  8243  ltletr  8244  readdcan  8294  addcan  8334  addcan2  8335  ltadd2  8574  divmulassap  8850  xrlelttr  10010  xrltletr  10011  xaddass  10073  xleadd1a  10077  xlesubadd  10087  icoshftf1o  10195  difelfzle  10338  fzo1fzo0n0  10391  modqmuladdim  10597  modqmuladdnn0  10598  modqm1p1mod0  10605  q2submod  10615  modifeq2int  10616  modqaddmulmod  10621  seq1g  10693  seqp1g  10696  ltexp2a  10821  exple1  10825  expnlbnd2  10895  nn0ltexp2  10939  nn0leexp2  10940  mulsubdivbinom2ap  10941  expcan  10946  fiprsshashgt1  11047  fun2dmnop0  11077  ccatass  11151  fzowrddc  11187  swrdclg  11190  ccatopth  11256  pfxccatin12lem2a  11267  pfxccat3  11274  maxleastb  11733  maxltsup  11737  xrltmaxsup  11776  xrmaxltsup  11777  xrmaxaddlem  11779  xrmaxadd  11780  addcn2  11829  mulcn2  11831  isumz  11908  dvdsmodexp  12314  modmulconst  12342  dvdsmod  12381  divalglemex  12441  divalg  12443  gcdass  12544  rplpwr  12556  rppwr  12557  nnwodc  12565  uzwodc  12566  rpmulgcd2  12625  rpdvds  12629  rpexp  12683  znege1  12708  prmdiveq  12766  hashgcdlem  12768  coprimeprodsq  12788  coprimeprodsq2  12789  pythagtriplem3  12798  pcdvdsb  12851  pcgcd1  12859  dvdsprmpweq  12866  pcbc  12882  ctinf  13009  nninfdc  13032  isnsgrp  13447  issubmnd  13483  mulgnn0p1  13678  mulgnnsubcl  13679  mulgneg  13685  mulgdirlem  13698  nmzsubg  13755  ghmmulg  13801  ring1eq0  14019  rmodislmod  14323  lspss  14371  2idlcpblrng  14495  neiint  14827  topssnei  14844  cnptopco  14904  cnrest2  14918  cnptoprest  14921  upxp  14954  bldisj  15083  blgt0  15084  bl2in  15085  blss2ps  15088  blss2  15089  xblm  15099  blssps  15109  blss  15110  bdmopn  15186  metcnp2  15195  txmetcnp  15200  cncfmptc  15278  dvcnp2cntop  15381  dvcn  15382  ply1term  15425  dvply1  15447  logdivlti  15563  ltexp2  15623  lgsfvalg  15692  lgsneg  15711  lgsmod  15713  lgsdilem  15714  lgsdirprm  15721  lgsdir  15722  lgsdi  15724  lgsne0  15725  1dom1el  16378