Theorem simpl3 1005

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

Assertion

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

Proof of Theorem simpl3

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

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

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 983

This theorem is referenced by:  simpll3  1041  simprl3  1047  simp1l3  1095  simp2l3  1101  simp3l3  1107  3anandirs  1361  ifnetruedc  3614  frirrg  4401  fcofo  5860  acexmid  5950  rdgon  6479  oawordi  6562  nnmord  6610  nnmword  6611  fidifsnen  6974  dif1en  6983  ac6sfi  7002  difinfsn  7209  2omotaplemap  7376  enq0tr  7554  distrlem4prl  7704  distrlem4pru  7705  ltaprg  7739  lelttr  8168  ltletr  8169  readdcan  8219  addcan  8259  addcan2  8260  ltadd2  8499  divmulassap  8775  xrlelttr  9935  xrltletr  9936  xaddass  9998  xleadd1a  10002  xlesubadd  10012  icoshftf1o  10120  difelfzle  10263  fzo1fzo0n0  10314  modqmuladdim  10519  modqmuladdnn0  10520  modqm1p1mod0  10527  q2submod  10537  modifeq2int  10538  modqaddmulmod  10543  seq1g  10615  seqp1g  10618  ltexp2a  10743  exple1  10747  expnlbnd2  10817  nn0ltexp2  10861  nn0leexp2  10862  mulsubdivbinom2ap  10863  expcan  10868  fiprsshashgt1  10969  fun2dmnop0  10999  ccatass  11072  fzowrddc  11108  swrdclg  11111  maxleastb  11569  maxltsup  11573  xrltmaxsup  11612  xrmaxltsup  11613  xrmaxaddlem  11615  xrmaxadd  11616  addcn2  11665  mulcn2  11667  isumz  11744  dvdsmodexp  12150  modmulconst  12178  dvdsmod  12217  divalglemex  12277  divalg  12279  gcdass  12380  rplpwr  12392  rppwr  12393  nnwodc  12401  uzwodc  12402  rpmulgcd2  12461  rpdvds  12465  rpexp  12519  znege1  12544  prmdiveq  12602  hashgcdlem  12604  coprimeprodsq  12624  coprimeprodsq2  12625  pythagtriplem3  12634  pcdvdsb  12687  pcgcd1  12695  dvdsprmpweq  12702  pcbc  12718  ctinf  12845  nninfdc  12868  isnsgrp  13282  issubmnd  13318  mulgnn0p1  13513  mulgnnsubcl  13514  mulgneg  13520  mulgdirlem  13533  nmzsubg  13590  ghmmulg  13636  ring1eq0  13854  rmodislmod  14157  lspss  14205  2idlcpblrng  14329  neiint  14661  topssnei  14678  cnptopco  14738  cnrest2  14752  cnptoprest  14755  upxp  14788  bldisj  14917  blgt0  14918  bl2in  14919  blss2ps  14922  blss2  14923  xblm  14933  blssps  14943  blss  14944  bdmopn  15020  metcnp2  15029  txmetcnp  15034  cncfmptc  15112  dvcnp2cntop  15215  dvcn  15216  ply1term  15259  dvply1  15281  logdivlti  15397  ltexp2  15457  lgsfvalg  15526  lgsneg  15545  lgsmod  15547  lgsdilem  15548  lgsdirprm  15555  lgsdir  15556  lgsdi  15558  lgsne0  15559  1dom1el  16001