Theorem simpl3l 1109

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpl3l	⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Proof of Theorem simpl3l

Step	Hyp	Ref	Expression
1		simp3l 1082	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	adantr 480	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  tfisi  6950  omopth2  7551  ltmul1a  10751  xaddass  11951  xlemul2a  11991  swrdsbslen  13300  dvdsadd2b  14866  pockthg  15448  psgnunilem4  17740  efgred  17984  ptbasin  21190  basqtop  21324  xrsmopn  22423  axpasch  25621  axcontlem4  25647  br4  30901  btwnintr  31296  btwnexch3  31297  btwnouttr2  31299  cgrxfr  31332  lineext  31353  btwnconn1lem13  31376  btwnconn1lem14  31377  btwnconn3  31380  brsegle  31385  brsegle2  31386  segleantisym  31392  outsideofeu  31408  lineunray  31424  lineelsb2  31425  cvrcmp  33588  atcvrj2b  33736  3dimlem3  33765  3dimlem3OLDN  33766  3dim3  33773  ps-1  33781  lplnnle2at  33845  2llnm3N  33873  lvolnle3at  33886  4atlem0a  33897  4atlem3  33900  4atlem3a  33901  lnatexN  34083  paddasslem8  34131  paddasslem9  34132  paddasslem10  34133  paddasslem12  34135  paddasslem13  34136  lhp2lt  34305  lhpexle2lem  34313  lhpexle3  34316  lhpmcvr3  34329  lhpat3  34350  4atex  34380  trlval2  34468  ltrnideq  34480  ltrnatlw  34488  trlnle  34491  trlval4  34493  cdlemd4  34506  cdlemd5  34507  cdleme16  34590  cdleme21  34643  cdleme21k  34644  cdleme27cl  34672  cdleme27N  34675  cdleme29ex  34680  cdleme43fsv1snlem  34726  cdleme40m  34773  cdleme46f2g2  34799  cdleme46f2g1  34800  trlord  34875  cdlemg8  34937  cdlemg15a  34961  cdlemg16z  34965  cdlemg18a  34984  cdlemg24  34994  cdlemg38  35021  cdlemg40  35023  trlcone  35034  cdlemj2  35128  tendoid0  35131  tendoconid  35135  cdlemk34  35216  cdlemk38  35221  cdlemkid4  35240  cdlemk35s-id  35244  cdlemk39s-id  35246  cdlemk53  35263  tendospcanN  35330  cdlemm10N  35425  dihvalcqpre  35542  dihopelvalcpre  35555  dihord5b  35566  dihglblem5apreN  35598  dihmeetlem16N  35629  dihmeetlem17N  35630  dvh3dim3N  35756  qirropth  36491  mzpcong  36557  jm2.26  36587  aomclem6  36647  limcleqr  38711  fourierdlem42  39042