Theorem simpl3 1004

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

Assertion

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

Proof of Theorem simpl3

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

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

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 982

This theorem is referenced by:  simpll3  1040  simprl3  1046  simp1l3  1094  simp2l3  1100  simp3l3  1106  3anandirs  1359  ifnetruedc  3603  frirrg  4386  fcofo  5834  acexmid  5924  rdgon  6453  oawordi  6536  nnmord  6584  nnmword  6585  fidifsnen  6940  dif1en  6949  ac6sfi  6968  difinfsn  7175  2omotaplemap  7342  enq0tr  7520  distrlem4prl  7670  distrlem4pru  7671  ltaprg  7705  lelttr  8134  ltletr  8135  readdcan  8185  addcan  8225  addcan2  8226  ltadd2  8465  divmulassap  8741  xrlelttr  9900  xrltletr  9901  xaddass  9963  xleadd1a  9967  xlesubadd  9977  icoshftf1o  10085  difelfzle  10228  fzo1fzo0n0  10278  modqmuladdim  10478  modqmuladdnn0  10479  modqm1p1mod0  10486  q2submod  10496  modifeq2int  10497  modqaddmulmod  10502  seq1g  10574  seqp1g  10577  ltexp2a  10702  exple1  10706  expnlbnd2  10776  nn0ltexp2  10820  nn0leexp2  10821  mulsubdivbinom2ap  10822  expcan  10827  fiprsshashgt1  10928  maxleastb  11398  maxltsup  11402  xrltmaxsup  11441  xrmaxltsup  11442  xrmaxaddlem  11444  xrmaxadd  11445  addcn2  11494  mulcn2  11496  isumz  11573  dvdsmodexp  11979  modmulconst  12007  dvdsmod  12046  divalglemex  12106  divalg  12108  gcdass  12209  rplpwr  12221  rppwr  12222  nnwodc  12230  uzwodc  12231  rpmulgcd2  12290  rpdvds  12294  rpexp  12348  znege1  12373  prmdiveq  12431  hashgcdlem  12433  coprimeprodsq  12453  coprimeprodsq2  12454  pythagtriplem3  12463  pcdvdsb  12516  pcgcd1  12524  dvdsprmpweq  12531  pcbc  12547  ctinf  12674  nninfdc  12697  isnsgrp  13110  issubmnd  13146  mulgnn0p1  13341  mulgnnsubcl  13342  mulgneg  13348  mulgdirlem  13361  nmzsubg  13418  ghmmulg  13464  ring1eq0  13682  rmodislmod  13985  lspss  14033  2idlcpblrng  14157  neiint  14489  topssnei  14506  cnptopco  14566  cnrest2  14580  cnptoprest  14583  upxp  14616  bldisj  14745  blgt0  14746  bl2in  14747  blss2ps  14750  blss2  14751  xblm  14761  blssps  14771  blss  14772  bdmopn  14848  metcnp2  14857  txmetcnp  14862  cncfmptc  14940  dvcnp2cntop  15043  dvcn  15044  ply1term  15087  dvply1  15109  logdivlti  15225  ltexp2  15285  lgsfvalg  15354  lgsneg  15373  lgsmod  15375  lgsdilem  15376  lgsdirprm  15383  lgsdir  15384  lgsdi  15386  lgsne0  15387  1dom1el  15745