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 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl3l  1083  simpr3l  1089  simp13l  1143  simp23l  1149  simp33l  1155  issod  4464  tfisi  4734  tfrlem5  6585  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  ecopovtrn  6906  ecopovtrng  6909  dftap2  7617  addassnqg  7749  ltsonq  7765  ltanqg  7767  ltmnqg  7768  addassnq0  7829  mulasssrg  8125  distrsrg  8126  lttrsr  8129  ltsosr  8131  ltasrg  8137  mulextsr1lem  8147  mulextsr1  8148  axmulass  8240  axdistr  8241  lemul1  8922  reapmul1lem  8923  reapmul1  8924  mulcanap  8994  mulcanap2  8995  divassap  9021  divdirap  9028  div11ap  9031  muldivdirap  9038  divcanap5  9045  apmul1  9119  apmul2  9120  ltdiv1  9199  ltmuldiv  9205  ledivmul  9208  lemuldiv  9212  ltdiv2  9218  lediv2  9222  ltdiv23  9223  lediv23  9224  xaddass2  10274  xlt2add  10284  modqdi  10831  expaddzap  11022  expmulzap  11024  leisorel  11291  resqrtcl  11797  xrbdtri  12044  dvdscmulr  12589  dvdsmulcr  12590  dvdsadd2b  12609  dvdsgcd  12791  rpexp12i  12935  pythagtriplem3  13048  pcpremul  13074  pceu  13076  pcqmul  13084  pcqdiv  13088  f1ocpbllem  13633  ercpbl  13654  erlecpbl  13655  cmn4  14110  ablsub4  14119  abladdsub4  14120  lidlsubcl  14826  psmetlecl  15437  xmetlecl  15470  wlkl1loop  16611