Theorem an4s 588

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 586	. 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  589  anandis  592  anandirs  593  trin2  5020  fnun  5322  2elresin  5327  f1co  5433  f1oun  5481  f1oco  5484  f1mpt  5771  poxp  6232  tfrlem7  6317  brecop  6624  th3qlem1  6636  oviec  6640  pmss12g  6674  addcmpblnq  7365  mulcmpblnq  7366  mulpipqqs  7371  mulclnq  7374  mulcanenq  7383  distrnqg  7385  mulcmpblnq0  7442  mulcanenq0ec  7443  mulclnq0  7450  nqnq0a  7452  nqnq0m  7453  distrnq0  7457  genipv  7507  genpelvl  7510  genpelvu  7511  genpml  7515  genpmu  7516  genpcdl  7517  genpcuu  7518  genprndl  7519  genprndu  7520  distrlem1prl  7580  distrlem1pru  7581  ltsopr  7594  addcmpblnr  7737  ltsrprg  7745  addclsr  7751  mulclsr  7752  addasssrg  7754  addresr  7835  mulresr  7836  axaddass  7870  axmulass  7871  axdistr  7872  mulgt0  8031  mul4  8088  add4  8117  2addsub  8170  addsubeq4  8171  sub4  8201  muladd  8340  mulsub  8357  add20i  8448  mulge0i  8576  mulap0b  8611  divmuldivap  8668  ltmul12a  8816  zmulcl  9305  uz2mulcl  9607  qaddcl  9634  qmulcl  9636  qreccl  9641  rpaddcl  9676  ge0addcl  9980  ge0xaddcl  9982  expge1  10556  rexanuz  10996  amgm2  11126  iooinsup  11284  mulcn2  11319  dvds2ln  11830  opoe  11899  omoe  11900  opeo  11901  omeo  11902  lcmgcd  12077  lcmdvds  12078  pc2dvds  12328  tgcl  13534  innei  13633  txbas  13728  txss12  13736  txbasval  13737  blsscls2  13963  qtopbasss  13991  lgslem3  14373  bj-indind  14654