Theorem simpl22 1253

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

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

Proof of Theorem simpl22

Step	Hyp	Ref	Expression
1		simpl2 1193	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl2 1187	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:  brbtwn2  28894  ax5seg  28927  axpasch  28930  axeuclid  28952  br8d  32602  br8  35811  cgrextend  36063  segconeq  36065  trisegint  36083  ifscgr  36099  cgrsub  36100  cgrxfr  36110  lineext  36131  seglecgr12im  36165  segletr  36169  lineunray  36202  lineelsb2  36203  cvrcmp  39392  cvlatexch3  39447  cvlsupr2  39452  atcvrj2b  39541  atexchcvrN  39549  3dim1  39576  3dim2  39577  3atlem3  39594  3atlem5  39596  lplnnle2at  39650  2llnjaN  39675  4atlem3  39705  4atlem10b  39714  4atlem12  39721  2llnma3r  39897  paddasslem4  39932  paddasslem7  39935  paddasslem8  39936  paddasslem12  39940  paddasslem13  39941  paddasslem15  39943  pmodlem1  39955  pmodlem2  39956  atmod1i1m  39967  llnexchb2lem  39977  4atex2  40186  ltrnatlw  40292  trlval4  40297  arglem1N  40299  cdlemd4  40310  cdlemd5  40311  cdleme0moN  40334  cdleme16  40394  cdleme20  40433  cdleme21k  40447  cdleme27N  40478  cdleme28c  40481  cdleme43fsv1snlem  40529  cdleme38n  40573  cdleme40n  40577  cdleme41snaw  40585  cdlemg6c  40729  cdlemg8c  40738  cdlemg8  40740  cdlemg12e  40756  cdlemg16  40766  cdlemg16ALTN  40767  cdlemg16z  40768  cdlemg16zz  40769  cdlemg18a  40787  cdlemg20  40794  cdlemg22  40796  cdlemg37  40798  cdlemg31d  40809  cdlemg33  40820  cdlemg38  40824  cdlemg44b  40841  cdlemk38  41024  cdlemk35s-id  41047  cdlemk39s-id  41049  cdlemk53b  41065  cdlemk55  41070  cdlemk35u  41073  cdlemk55u  41075  cdlemn11pre  41319