Theorem an4s 553

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 551	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
2		an4s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
3	1, 2	sylbi 119	1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  an42s  554  anandis  557  anandirs  558  trin2  4786  fnun  5081  2elresin  5086  f1co  5184  f1oun  5229  f1oco  5232  f1mpt  5504  poxp  5947  tfrlem7  6029  brecop  6327  th3qlem1  6339  oviec  6343  pmss12g  6377  addcmpblnq  6862  mulcmpblnq  6863  mulpipqqs  6868  mulclnq  6871  mulcanenq  6880  distrnqg  6882  mulcmpblnq0  6939  mulcanenq0ec  6940  mulclnq0  6947  nqnq0a  6949  nqnq0m  6950  distrnq0  6954  genipv  7004  genpelvl  7007  genpelvu  7008  genpml  7012  genpmu  7013  genpcdl  7014  genpcuu  7015  genprndl  7016  genprndu  7017  distrlem1prl  7077  distrlem1pru  7078  ltsopr  7091  addcmpblnr  7221  ltsrprg  7229  addclsr  7235  mulclsr  7236  addasssrg  7238  addresr  7310  mulresr  7311  axaddass  7343  axmulass  7344  axdistr  7345  mulgt0  7496  mul4  7550  add4  7579  2addsub  7632  addsubeq4  7633  sub4  7663  muladd  7798  mulsub  7815  add20i  7903  mulge0i  8030  mulap0b  8055  divmuldivap  8110  ltmul12a  8248  zmulcl  8728  uz2mulcl  9019  qaddcl  9044  qmulcl  9046  qreccl  9051  rpaddcl  9081  ge0addcl  9323  serige0  9842  expge1  9882  rexanuz  10308  amgm2  10438  mulcn2  10585  dvds2ln  10695  opoe  10761  omoe  10762  opeo  10763  omeo  10764  lcmgcd  10926  lcmdvds  10927  bj-indind  11256