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 2275  wefrc 2943  f1oweALT 3906  tfrlem1 3911  tfrlem9 3919  tz7.49 3959  oaordex 4192  aceq6b 4742  zorn2lem4 4791  zorn2lem7 4794  psslinpr 5135  prlem936 5155  mulcant 5690  divdirt 5750  lemul1it 5837  ltdiv1t 5849  ltmuldivt 5863  ltdiv2t 5887  facwordit 6944  cvgratlem1 7250  elcls 7704  elcls3 7711  islp2 7747  rnblssm 7851  neibl 7877  metcnp4lem2 7969  nmoubi 8435  blocnilem 8464  ubthlem14 8542  nmopubt 9832  nmfnleubt 9849  branmfnt 10038  atcvatlem 10312  atcvat4 10324  and4as 10432

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