Theorem simpl3 1029

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

Assertion

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

Proof of Theorem simpl3

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

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

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 1007

This theorem is referenced by:  simpll3  1065  simprl3  1071  simp1l3  1119  simp2l3  1125  simp3l3  1131  3anandirs  1385  ifnetruedc  3670  frirrg  4476  fcofo  5963  acexmid  6057  rdgon  6630  oawordi  6715  nnmord  6763  nnmword  6764  1dom1el  7073  mapunen  7117  fidifsnen  7138  dif1en  7149  ac6sfi  7168  fissfi  7229  difinfsn  7404  2omotaplemap  7587  enq0tr  7765  distrlem4prl  7915  distrlem4pru  7916  ltaprg  7950  lelttr  8378  ltletr  8379  readdcan  8430  addcan  8470  addcan2  8471  ltadd2  8711  divmulassap  8989  xrlelttr  10161  xrltletr  10162  xaddass  10224  xleadd1a  10228  xlesubadd  10238  icoshftf1o  10346  lincmble  10359  difelfzle  10493  fzo1fzo0n0  10547  modqmuladdim  10756  modqmuladdnn0  10757  modqm1p1mod0  10764  q2submod  10774  modifeq2int  10775  modqaddmulmod  10780  seq1g  10852  seqp1g  10855  ltexp2a  10980  exple1  10984  expnlbnd2  11055  nn0ltexp2  11099  nn0leexp2  11100  mulsubdivbinom2ap  11101  expcan  11106  fiprsshashgt1  11210  hashtpgim  11245  hashtpg  11247  fun2dmnop0  11250  ccatass  11324  fzowrddc  11367  swrdclg  11370  ccatopth  11436  pfxccatin12lem2a  11447  pfxccat3  11454  maxleastb  11927  maxltsup  11931  xrltmaxsup  11970  xrmaxltsup  11971  xrmaxaddlem  11973  xrmaxadd  11974  addcn2  12023  mulcn2  12025  isumz  12103  dvdsmodexp  12509  modmulconst  12537  dvdsmod  12576  divalglemex  12636  divalg  12638  gcdass  12739  rplpwr  12751  rppwr  12752  nnwodc  12760  uzwodc  12761  rpmulgcd2  12820  rpdvds  12824  rpexp  12878  znege1  12903  prmdiveq  12961  hashgcdlem  12963  coprimeprodsq  12983  coprimeprodsq2  12984  pythagtriplem3  12993  pcdvdsb  13046  pcgcd1  13054  dvdsprmpweq  13061  pcbc  13077  ctinf  13268  nninfdc  13291  isnsgrp  13672  issubmnd  13706  mulgnn0p1  13889  mulgnnsubcl  13890  mulgneg  13896  mulgdirlem  13909  nmzsubg  13966  ghmmulg  14012  gfsumsn  14110  ring1eq0  14294  rmodislmod  14628  lspss  14676  2idlcpblrng  14800  neiint  15139  topssnei  15156  cnptopco  15216  cnrest2  15230  cnptoprest  15233  upxp  15266  bldisj  15395  blgt0  15396  bl2in  15397  blss2ps  15400  blss2  15401  xblm  15411  blssps  15421  blss  15422  bdmopn  15498  metcnp2  15507  txmetcnp  15512  cncfmptc  15590  dvcnp2cntop  15693  dvcn  15694  ply1term  15737  dvply1  15759  logdivlti  15875  ltexp2  15935  pellexlem2  15975  lgsfvalg  16007  lgsneg  16026  lgsmod  16028  lgsdilem  16029  lgsdirprm  16036  lgsdir  16037  lgsdi  16039  lgsne0  16040