Theorem simp3l 1056

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

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

Proof of Theorem simp3l

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2ant3 1051	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

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

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 1011

This theorem is referenced by:  simpl3l  1083  simpr3l  1089  simp13l  1143  simp23l  1149  simp33l  1155  issod  4462  tfisi  4732  tfrlem5  6579  tfrlemibxssdm  6592  tfr1onlembxssdm  6608  tfrcllembxssdm  6621  ecopovtrn  6900  ecopovtrng  6903  dftap2  7611  addassnqg  7743  ltsonq  7759  ltanqg  7761  ltmnqg  7762  addassnq0  7823  mulasssrg  8119  distrsrg  8120  lttrsr  8123  ltsosr  8125  ltasrg  8131  mulextsr1lem  8141  mulextsr1  8142  axmulass  8234  axdistr  8235  lemul1  8915  reapmul1lem  8916  reapmul1  8917  mulcanap  8987  mulcanap2  8988  divassap  9014  divdirap  9021  div11ap  9024  muldivdirap  9031  divcanap5  9038  apmul1  9112  apmul2  9113  ltdiv1  9192  ltmuldiv  9198  ledivmul  9201  lemuldiv  9205  ltdiv2  9211  lediv2  9215  ltdiv23  9216  lediv23  9217  xaddass2  10255  xlt2add  10265  modqdi  10812  expaddzap  11003  expmulzap  11005  leisorel  11272  resqrtcl  11778  xrbdtri  12025  dvdscmulr  12570  dvdsmulcr  12571  dvdsadd2b  12590  dvdsgcd  12772  rpexp12i  12916  pythagtriplem3  13029  pcpremul  13055  pceu  13057  pcqmul  13065  pcqdiv  13069  f1ocpbllem  13614  ercpbl  13635  erlecpbl  13636  cmn4  14091  ablsub4  14100  abladdsub4  14101  lidlsubcl  14807  psmetlecl  15418  xmetlecl  15451  wlkl1loop  16582