Theorem simp2rl 1243

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

Assertion

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

Proof of Theorem simp2rl

Step	Hyp	Ref	Expression
1		simprl 770	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant2 1134	1 ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  tfrlem5  8348  omeu  8549  wemaplem3  9501  gruina  10771  expmordi  14132  4sqlem18  16933  vdwlem10  16961  mdetuni0  22508  mdetmul  22510  tsmsxp  24042  ax5seglem3  28858  btwnconn1lem1  36075  btwnconn1lem2  36076  btwnconn1lem3  36077  btwnconn1lem4  36078  btwnconn1lem12  36086  btwnconn1lem13  36087  linethru  36141  2llnjN  39561  2lplnja  39613  2lplnj  39614  cdlemblem  39787  dalaw  39880  pclfinN  39894  lhpmcvr4N  40020  lhp2atne  40028  lhp2at0ne  40030  cdlemb2  40035  cdlemd7  40198  cdleme01N  40215  cdleme02N  40216  cdleme0ex2N  40218  cdleme7aa  40236  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme11a  40254  cdleme20k  40313  cdleme21d  40324  cdleme27cl  40360  cdlemefrs29bpre0  40390  cdlemefrs29cpre1  40392  cdlemefrs32fva  40394  cdlemefrs32fva1  40395  cdlemefr29exN  40396  cdlemefr32sn2aw  40398  cdlemefr31fv1  40405  cdlemefs32sn1aw  40408  cdlemefr44  40419  cdlemefr45e  40422  cdleme41sn3a  40427  cdleme35a  40442  cdleme35fnpq  40443  cdleme35b  40444  cdleme35c  40445  cdleme35d  40446  cdleme35e  40447  cdleme35f  40448  cdleme35sn3a  40453  cdleme42e  40473  cdleme42h  40476  cdleme42i  40477  cdleme17d2  40489  cdleme48fv  40493  cdleme48bw  40496  cdleme48b  40497  cdlemeg46c  40507  cdlemeg46ngfr  40512  cdleme48d  40529  cdlemg2kq  40596  cdlemg2m  40598  cdlemg7fvN  40618  cdlemg8a  40621  cdlemg11aq  40632  cdlemg10c  40633  cdlemg17a  40655  cdlemg31b0N  40688  cdlemg41  40712  cdlemh2  40810  cdlemi  40814  cdlemk21-2N  40885  dihmeetlem1N  41284  dihmeetlem13N  41313  iunrelexpmin1  43697