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  8299  omeu  8500  wemaplem3  9434  gruina  10706  expmordi  14071  4sqlem18  16871  vdwlem10  16899  mdetuni0  22534  mdetmul  22536  tsmsxp  24068  ax5seglem3  28907  btwnconn1lem1  36120  btwnconn1lem2  36121  btwnconn1lem3  36122  btwnconn1lem4  36123  btwnconn1lem12  36131  btwnconn1lem13  36132  linethru  36186  2llnjN  39605  2lplnja  39657  2lplnj  39658  cdlemblem  39831  dalaw  39924  pclfinN  39938  lhpmcvr4N  40064  lhp2atne  40072  lhp2at0ne  40074  cdlemb2  40079  cdlemd7  40242  cdleme01N  40259  cdleme02N  40260  cdleme0ex2N  40262  cdleme7aa  40280  cdleme7c  40283  cdleme7d  40284  cdleme7e  40285  cdleme7ga  40286  cdleme11a  40298  cdleme20k  40357  cdleme21d  40368  cdleme27cl  40404  cdlemefrs29bpre0  40434  cdlemefrs29cpre1  40436  cdlemefrs32fva  40438  cdlemefrs32fva1  40439  cdlemefr29exN  40440  cdlemefr32sn2aw  40442  cdlemefr31fv1  40449  cdlemefs32sn1aw  40452  cdlemefr44  40463  cdlemefr45e  40466  cdleme41sn3a  40471  cdleme35a  40486  cdleme35fnpq  40487  cdleme35b  40488  cdleme35c  40489  cdleme35d  40490  cdleme35e  40491  cdleme35f  40492  cdleme35sn3a  40497  cdleme42e  40517  cdleme42h  40520  cdleme42i  40521  cdleme17d2  40533  cdleme48fv  40537  cdleme48bw  40540  cdleme48b  40541  cdlemeg46c  40551  cdlemeg46ngfr  40556  cdleme48d  40573  cdlemg2kq  40640  cdlemg2m  40642  cdlemg7fvN  40662  cdlemg8a  40665  cdlemg11aq  40676  cdlemg10c  40677  cdlemg17a  40699  cdlemg31b0N  40732  cdlemg41  40756  cdlemh2  40854  cdlemi  40858  cdlemk21-2N  40929  dihmeetlem1N  41328  dihmeetlem13N  41357  iunrelexpmin1  43740