Theorem simp3r 1057

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

Assertion

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

Proof of Theorem simp3r

Step	Hyp	Ref	Expression
1		simpr 110	. 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:  simpl3r  1084  simpr3r  1090  simp13r  1144  simp23r  1150  simp33r  1156  issod  4464  tfisi  4734  fvun1  5769  f1oiso2  6033  tfrlem5  6585  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  ecopovtrn  6906  ecopovtrng  6909  dftap2  7618  addassnqg  7750  ltsonq  7766  ltanqg  7768  ltmnqg  7769  addassnq0  7830  mulasssrg  8126  distrsrg  8127  lttrsr  8130  ltsosr  8132  ltasrg  8138  mulextsr1lem  8148  mulextsr1  8149  axmulass  8241  axdistr  8242  reapmul1  8926  mulcanap  8996  mulcanap2  8997  divassap  9023  divdirap  9030  div11ap  9033  apmul1  9121  ltdiv1  9201  ltmuldiv  9207  ledivmul  9210  lemuldiv  9214  lediv2  9224  ltdiv23  9225  lediv23  9226  xaddass2  10283  xlt2add  10293  modqdi  10843  expaddzap  11034  expmulzap  11036  leisorel  11304  resqrtcl  11810  xrbdtri  12060  dvdsgcd  12807  rpexp12i  12952  pythagtriplem4  13069  pythagtriplem11  13075  pythagtriplem13  13077  pcpremul  13094  pceu  13096  pcqmul  13104  pcqdiv  13108  f1ocpbllem  13682  ercpbl  13703  erlecpbl  13704  cmn4  14159  ablsub4  14168  abladdsub4  14169  lidlsubcl  14875  psmetlecl  15487  xmetlecl  15520  xblcntrps  15566  xblcntr  15567