Theorem an4s 592

Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)

Hypothesis

Ref	Expression
an4s.1	⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)

Assertion

Ref	Expression
an4s	⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)

Proof of Theorem an4s

Step	Hyp	Ref	Expression
1		an4 588	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
2		an4s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
3	1, 2	sylbi 121	1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  an42s  593  anandis  596  anandirs  597  trin2  5128  fnun  5438  2elresin  5443  f1co  5554  f1oun  5603  f1oco  5606  f1mpt  5911  poxp  6396  tfrlem7  6482  brecop  6793  th3qlem1  6805  oviec  6809  pmss12g  6843  addcmpblnq  7586  mulcmpblnq  7587  mulpipqqs  7592  mulclnq  7595  mulcanenq  7604  distrnqg  7606  mulcmpblnq0  7663  mulcanenq0ec  7664  mulclnq0  7671  nqnq0a  7673  nqnq0m  7674  distrnq0  7678  genipv  7728  genpelvl  7731  genpelvu  7732  genpml  7736  genpmu  7737  genpcdl  7738  genpcuu  7739  genprndl  7740  genprndu  7741  distrlem1prl  7801  distrlem1pru  7802  ltsopr  7815  addcmpblnr  7958  ltsrprg  7966  addclsr  7972  mulclsr  7973  addasssrg  7975  addresr  8056  mulresr  8057  axaddass  8091  axmulass  8092  axdistr  8093  mulgt0  8253  mul4  8310  add4  8339  2addsub  8392  addsubeq4  8393  sub4  8423  muladd  8562  mulsub  8579  add20i  8671  mulge0i  8799  mulap0b  8834  divmuldivap  8891  ltmul12a  9039  zmulcl  9532  uz2mulcl  9841  qaddcl  9868  qmulcl  9870  qreccl  9875  rpaddcl  9911  ge0addcl  10215  ge0xaddcl  10217  expge1  10837  rexanuz  11548  amgm2  11678  iooinsup  11837  mulcn2  11872  dvds2ln  12384  opoe  12455  omoe  12456  opeo  12457  omeo  12458  lcmgcd  12649  lcmdvds  12650  pc2dvds  12902  tgcl  14787  innei  14886  txbas  14981  txss12  14989  txbasval  14990  blsscls2  15216  qtopbasss  15244  lgslem3  15730  bj-indind  16527