Theorem simp3r 1028

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

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

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 982

This theorem is referenced by:  simpl3r  1055  simpr3r  1061  simp13r  1115  simp23r  1121  simp33r  1127  issod  4354  tfisi  4623  fvun1  5627  f1oiso2  5874  tfrlem5  6372  tfr1onlembxssdm  6401  tfrcllembxssdm  6414  ecopovtrn  6691  ecopovtrng  6694  dftap2  7318  addassnqg  7449  ltsonq  7465  ltanqg  7467  ltmnqg  7468  addassnq0  7529  mulasssrg  7825  distrsrg  7826  lttrsr  7829  ltsosr  7831  ltasrg  7837  mulextsr1lem  7847  mulextsr1  7848  axmulass  7940  axdistr  7941  reapmul1  8622  mulcanap  8692  mulcanap2  8693  divassap  8717  divdirap  8724  div11ap  8727  apmul1  8815  ltdiv1  8895  ltmuldiv  8901  ledivmul  8904  lemuldiv  8908  lediv2  8918  ltdiv23  8919  lediv23  8920  xaddass2  9945  xlt2add  9955  modqdi  10484  expaddzap  10675  expmulzap  10677  leisorel  10929  resqrtcl  11194  xrbdtri  11441  dvdsgcd  12179  rpexp12i  12323  pythagtriplem4  12437  pythagtriplem11  12443  pythagtriplem13  12445  pcpremul  12462  pceu  12464  pcqmul  12472  pcqdiv  12476  f1ocpbllem  12953  ercpbl  12974  erlecpbl  12975  cmn4  13435  ablsub4  13443  abladdsub4  13444  lidlsubcl  14043  psmetlecl  14570  xmetlecl  14603  xblcntrps  14649  xblcntr  14650