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  3598  frirrg  4381  fcofo  5827  acexmid  5917  rdgon  6439  oawordi  6522  nnmord  6570  nnmword  6571  fidifsnen  6926  dif1en  6935  ac6sfi  6954  difinfsn  7159  2omotaplemap  7317  enq0tr  7494  distrlem4prl  7644  distrlem4pru  7645  ltaprg  7679  lelttr  8108  ltletr  8109  readdcan  8159  addcan  8199  addcan2  8200  ltadd2  8438  divmulassap  8714  xrlelttr  9872  xrltletr  9873  xaddass  9935  xleadd1a  9939  xlesubadd  9949  icoshftf1o  10057  difelfzle  10200  fzo1fzo0n0  10250  modqmuladdim  10438  modqmuladdnn0  10439  modqm1p1mod0  10446  q2submod  10456  modifeq2int  10457  modqaddmulmod  10462  seq1g  10534  seqp1g  10537  ltexp2a  10662  exple1  10666  expnlbnd2  10736  nn0ltexp2  10780  nn0leexp2  10781  mulsubdivbinom2ap  10782  expcan  10787  fiprsshashgt1  10888  maxleastb  11358  maxltsup  11362  xrltmaxsup  11400  xrmaxltsup  11401  xrmaxaddlem  11403  xrmaxadd  11404  addcn2  11453  mulcn2  11455  isumz  11532  dvdsmodexp  11938  modmulconst  11966  dvdsmod  12004  divalglemex  12063  divalg  12065  gcdass  12152  rplpwr  12164  rppwr  12165  nnwodc  12173  uzwodc  12174  rpmulgcd2  12233  rpdvds  12237  rpexp  12291  znege1  12316  prmdiveq  12374  hashgcdlem  12376  coprimeprodsq  12395  coprimeprodsq2  12396  pythagtriplem3  12405  pcdvdsb  12458  pcgcd1  12466  dvdsprmpweq  12473  pcbc  12489  ctinf  12587  nninfdc  12610  isnsgrp  12989  issubmnd  13023  mulgnn0p1  13203  mulgnnsubcl  13204  mulgneg  13210  mulgdirlem  13223  nmzsubg  13280  ghmmulg  13326  ring1eq0  13544  rmodislmod  13847  lspss  13895  2idlcpblrng  14019  neiint  14313  topssnei  14330  cnptopco  14390  cnrest2  14404  cnptoprest  14407  upxp  14440  bldisj  14569  blgt0  14570  bl2in  14571  blss2ps  14574  blss2  14575  xblm  14585  blssps  14595  blss  14596  bdmopn  14672  metcnp2  14681  txmetcnp  14686  cncfmptc  14750  dvcnp2cntop  14848  dvcn  14849  ply1term  14889  logdivlti  15016  ltexp2  15074  lgsfvalg  15121  lgsneg  15140  lgsmod  15142  lgsdilem  15143  lgsdirprm  15150  lgsdir  15151  lgsdi  15153  lgsne0  15154  1dom1el  15483