Theorem simpl3 1028

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

Assertion

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

Proof of Theorem simpl3

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

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

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 1006

This theorem is referenced by:  simpll3  1064  simprl3  1070  simp1l3  1118  simp2l3  1124  simp3l3  1130  3anandirs  1384  ifnetruedc  3649  frirrg  4447  fcofo  5925  acexmid  6017  rdgon  6552  oawordi  6637  nnmord  6685  nnmword  6686  1dom1el  6993  fidifsnen  7057  dif1en  7068  ac6sfi  7087  difinfsn  7299  2omotaplemap  7476  enq0tr  7654  distrlem4prl  7804  distrlem4pru  7805  ltaprg  7839  lelttr  8268  ltletr  8269  readdcan  8319  addcan  8359  addcan2  8360  ltadd2  8599  divmulassap  8875  xrlelttr  10041  xrltletr  10042  xaddass  10104  xleadd1a  10108  xlesubadd  10118  icoshftf1o  10226  difelfzle  10369  fzo1fzo0n0  10423  modqmuladdim  10630  modqmuladdnn0  10631  modqm1p1mod0  10638  q2submod  10648  modifeq2int  10649  modqaddmulmod  10654  seq1g  10726  seqp1g  10729  ltexp2a  10854  exple1  10858  expnlbnd2  10928  nn0ltexp2  10972  nn0leexp2  10973  mulsubdivbinom2ap  10974  expcan  10979  fiprsshashgt1  11082  fun2dmnop0  11112  ccatass  11186  fzowrddc  11229  swrdclg  11232  ccatopth  11298  pfxccatin12lem2a  11309  pfxccat3  11316  maxleastb  11776  maxltsup  11780  xrltmaxsup  11819  xrmaxltsup  11820  xrmaxaddlem  11822  xrmaxadd  11823  addcn2  11872  mulcn2  11874  isumz  11952  dvdsmodexp  12358  modmulconst  12386  dvdsmod  12425  divalglemex  12485  divalg  12487  gcdass  12588  rplpwr  12600  rppwr  12601  nnwodc  12609  uzwodc  12610  rpmulgcd2  12669  rpdvds  12673  rpexp  12727  znege1  12752  prmdiveq  12810  hashgcdlem  12812  coprimeprodsq  12832  coprimeprodsq2  12833  pythagtriplem3  12842  pcdvdsb  12895  pcgcd1  12903  dvdsprmpweq  12910  pcbc  12926  ctinf  13053  nninfdc  13076  isnsgrp  13491  issubmnd  13527  mulgnn0p1  13722  mulgnnsubcl  13723  mulgneg  13729  mulgdirlem  13742  nmzsubg  13799  ghmmulg  13845  ring1eq0  14064  rmodislmod  14368  lspss  14416  2idlcpblrng  14540  neiint  14872  topssnei  14889  cnptopco  14949  cnrest2  14963  cnptoprest  14966  upxp  14999  bldisj  15128  blgt0  15129  bl2in  15130  blss2ps  15133  blss2  15134  xblm  15144  blssps  15154  blss  15155  bdmopn  15231  metcnp2  15240  txmetcnp  15245  cncfmptc  15323  dvcnp2cntop  15426  dvcn  15427  ply1term  15470  dvply1  15492  logdivlti  15608  ltexp2  15668  lgsfvalg  15737  lgsneg  15756  lgsmod  15758  lgsdilem  15759  lgsdirprm  15766  lgsdir  15767  lgsdi  15769  lgsne0  15770  gfsumsn  16706