Theorem imp4a 364

Description: An importation inference.

Hypothesis

Ref	Expression
imp4.1	|- (ph -> (ps -> (ch -> (th -> ta))))

Assertion

Ref	Expression
imp4a	|- (ph -> (ps -> ((ch /\ th) -> ta)))

Proof of Theorem imp4a

Step	Hyp	Ref	Expression
1		imp4.1	. 2 |- (ph -> (ps -> (ch -> (th -> ta))))
2		impexp 347	. 2 |- (((ch /\ th) -> ta) <-> (ch -> (th -> ta)))
3	1, 2	syl6ibr 213	1 |- (ph -> (ps -> ((ch /\ th) -> ta)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  imp4b 365  imp4d 367  reuss2 2271  wefrc 2938  f1oweALT 3897  tfrlem1 3902  tfrlem9 3910  tz7.49 3950  oaordex 4182  aceq6b 4722  zorn2lem4 4771  zorn2lem7 4774  psslinpr 5115  prlem936 5135  lemul1it 5801  ltdiv2t 5843  facwordit 6889  cvgratlem1 7193  elcls 7654  elcls3 7661  islp2 7697  rnblssm 7803  neibl 7829  metcnp4lem2 7919  nmoubi 8380  blocnilem 8408  ubthlem14 8486  nmopubt 9772  nmfnleubt 9788  branmfnt 9976  atcvatlem 10249  atcvat4 10261  and4as 10368

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain