Theorem simpl3 1026

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

Assertion

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

Proof of Theorem simpl3

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

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

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 1004

This theorem is referenced by:  simpll3  1062  simprl3  1068  simp1l3  1116  simp2l3  1122  simp3l3  1128  3anandirs  1382  ifnetruedc  3646  frirrg  4442  fcofo  5917  acexmid  6009  rdgon  6543  oawordi  6628  nnmord  6676  nnmword  6677  fidifsnen  7045  dif1en  7054  ac6sfi  7073  difinfsn  7283  2omotaplemap  7459  enq0tr  7637  distrlem4prl  7787  distrlem4pru  7788  ltaprg  7822  lelttr  8251  ltletr  8252  readdcan  8302  addcan  8342  addcan2  8343  ltadd2  8582  divmulassap  8858  xrlelttr  10019  xrltletr  10020  xaddass  10082  xleadd1a  10086  xlesubadd  10096  icoshftf1o  10204  difelfzle  10347  fzo1fzo0n0  10400  modqmuladdim  10606  modqmuladdnn0  10607  modqm1p1mod0  10614  q2submod  10624  modifeq2int  10625  modqaddmulmod  10630  seq1g  10702  seqp1g  10705  ltexp2a  10830  exple1  10834  expnlbnd2  10904  nn0ltexp2  10948  nn0leexp2  10949  mulsubdivbinom2ap  10950  expcan  10955  fiprsshashgt1  11057  fun2dmnop0  11087  ccatass  11161  fzowrddc  11200  swrdclg  11203  ccatopth  11269  pfxccatin12lem2a  11280  pfxccat3  11287  maxleastb  11746  maxltsup  11750  xrltmaxsup  11789  xrmaxltsup  11790  xrmaxaddlem  11792  xrmaxadd  11793  addcn2  11842  mulcn2  11844  isumz  11921  dvdsmodexp  12327  modmulconst  12355  dvdsmod  12394  divalglemex  12454  divalg  12456  gcdass  12557  rplpwr  12569  rppwr  12570  nnwodc  12578  uzwodc  12579  rpmulgcd2  12638  rpdvds  12642  rpexp  12696  znege1  12721  prmdiveq  12779  hashgcdlem  12781  coprimeprodsq  12801  coprimeprodsq2  12802  pythagtriplem3  12811  pcdvdsb  12864  pcgcd1  12872  dvdsprmpweq  12879  pcbc  12895  ctinf  13022  nninfdc  13045  isnsgrp  13460  issubmnd  13496  mulgnn0p1  13691  mulgnnsubcl  13692  mulgneg  13698  mulgdirlem  13711  nmzsubg  13768  ghmmulg  13814  ring1eq0  14032  rmodislmod  14336  lspss  14384  2idlcpblrng  14508  neiint  14840  topssnei  14857  cnptopco  14917  cnrest2  14931  cnptoprest  14934  upxp  14967  bldisj  15096  blgt0  15097  bl2in  15098  blss2ps  15101  blss2  15102  xblm  15112  blssps  15122  blss  15123  bdmopn  15199  metcnp2  15208  txmetcnp  15213  cncfmptc  15291  dvcnp2cntop  15394  dvcn  15395  ply1term  15438  dvply1  15460  logdivlti  15576  ltexp2  15636  lgsfvalg  15705  lgsneg  15724  lgsmod  15726  lgsdilem  15727  lgsdirprm  15734  lgsdir  15735  lgsdi  15737  lgsne0  15738  1dom1el  16463