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  3650  frirrg  4449  fcofo  5930  acexmid  6022  rdgon  6557  oawordi  6642  nnmord  6690  nnmword  6691  1dom1el  6998  fidifsnen  7062  dif1en  7073  ac6sfi  7092  difinfsn  7304  2omotaplemap  7481  enq0tr  7659  distrlem4prl  7809  distrlem4pru  7810  ltaprg  7844  lelttr  8273  ltletr  8274  readdcan  8324  addcan  8364  addcan2  8365  ltadd2  8604  divmulassap  8880  xrlelttr  10046  xrltletr  10047  xaddass  10109  xleadd1a  10113  xlesubadd  10123  icoshftf1o  10231  difelfzle  10374  fzo1fzo0n0  10428  modqmuladdim  10635  modqmuladdnn0  10636  modqm1p1mod0  10643  q2submod  10653  modifeq2int  10654  modqaddmulmod  10659  seq1g  10731  seqp1g  10734  ltexp2a  10859  exple1  10863  expnlbnd2  10933  nn0ltexp2  10977  nn0leexp2  10978  mulsubdivbinom2ap  10979  expcan  10984  fiprsshashgt1  11087  hashtpgim  11115  hashtpg  11117  fun2dmnop0  11120  ccatass  11194  fzowrddc  11237  swrdclg  11240  ccatopth  11306  pfxccatin12lem2a  11317  pfxccat3  11324  maxleastb  11797  maxltsup  11801  xrltmaxsup  11840  xrmaxltsup  11841  xrmaxaddlem  11843  xrmaxadd  11844  addcn2  11893  mulcn2  11895  isumz  11973  dvdsmodexp  12379  modmulconst  12407  dvdsmod  12446  divalglemex  12506  divalg  12508  gcdass  12609  rplpwr  12621  rppwr  12622  nnwodc  12630  uzwodc  12631  rpmulgcd2  12690  rpdvds  12694  rpexp  12748  znege1  12773  prmdiveq  12831  hashgcdlem  12833  coprimeprodsq  12853  coprimeprodsq2  12854  pythagtriplem3  12863  pcdvdsb  12916  pcgcd1  12924  dvdsprmpweq  12931  pcbc  12947  ctinf  13074  nninfdc  13097  isnsgrp  13512  issubmnd  13548  mulgnn0p1  13743  mulgnnsubcl  13744  mulgneg  13750  mulgdirlem  13763  nmzsubg  13820  ghmmulg  13866  ring1eq0  14085  rmodislmod  14389  lspss  14437  2idlcpblrng  14561  neiint  14898  topssnei  14915  cnptopco  14975  cnrest2  14989  cnptoprest  14992  upxp  15025  bldisj  15154  blgt0  15155  bl2in  15156  blss2ps  15159  blss2  15160  xblm  15170  blssps  15180  blss  15181  bdmopn  15257  metcnp2  15266  txmetcnp  15271  cncfmptc  15349  dvcnp2cntop  15452  dvcn  15453  ply1term  15496  dvply1  15518  logdivlti  15634  ltexp2  15694  lgsfvalg  15763  lgsneg  15782  lgsmod  15784  lgsdilem  15785  lgsdirprm  15792  lgsdir  15793  lgsdi  15795  lgsne0  15796  gfsumsn  16753