Theorem simp3r 1029

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

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

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 983

This theorem is referenced by:  simpl3r  1056  simpr3r  1062  simp13r  1116  simp23r  1122  simp33r  1128  issod  4371  tfisi  4640  fvun1  5655  f1oiso2  5906  tfrlem5  6410  tfr1onlembxssdm  6439  tfrcllembxssdm  6452  ecopovtrn  6729  ecopovtrng  6732  dftap2  7376  addassnqg  7508  ltsonq  7524  ltanqg  7526  ltmnqg  7527  addassnq0  7588  mulasssrg  7884  distrsrg  7885  lttrsr  7888  ltsosr  7890  ltasrg  7896  mulextsr1lem  7906  mulextsr1  7907  axmulass  7999  axdistr  8000  reapmul1  8681  mulcanap  8751  mulcanap2  8752  divassap  8776  divdirap  8783  div11ap  8786  apmul1  8874  ltdiv1  8954  ltmuldiv  8960  ledivmul  8963  lemuldiv  8967  lediv2  8977  ltdiv23  8978  lediv23  8979  xaddass2  10005  xlt2add  10015  modqdi  10550  expaddzap  10741  expmulzap  10743  leisorel  10995  resqrtcl  11390  xrbdtri  11637  dvdsgcd  12383  rpexp12i  12527  pythagtriplem4  12641  pythagtriplem11  12647  pythagtriplem13  12649  pcpremul  12666  pceu  12668  pcqmul  12676  pcqdiv  12680  f1ocpbllem  13192  ercpbl  13213  erlecpbl  13214  cmn4  13691  ablsub4  13699  abladdsub4  13700  lidlsubcl  14299  psmetlecl  14856  xmetlecl  14889  xblcntrps  14935  xblcntr  14936