Theorem jctir 241

Description: Inference conjoining a theorem to right of consequent in an implication.

Hypotheses

Ref	Expression
jctir.1	|- (ph -> ps)
jctir.2	|- ch

Assertion

Ref	Expression
jctir	|- (ph -> (ps /\ ch))

Proof of Theorem jctir

Step	Hyp	Ref	Expression
1		jctir.1	. 2 |- (ph -> ps)
2		jctir.2	. . 3 |- ch
3	2	a1i 7	. 2 |- (ph -> ch)
4	1, 3	jca 236	1 |- (ph -> (ps /\ ch))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  eqvin.l1 851  supsn 2168  ordsseleq 2227  ordunidif 2260  onssmin 2263  fn0 2739  fnopabfv 2858  fsn 2895  tz7.44-3 2968  oawordeulem 3156  ssdomg 3311  limenpsi 3400  phplem5 3407  php 3409  ominf 3423  pssnn 3428  aceq3lem 3555  aceq6b 3565  fodomb 3615  cfsuc 3709  prlem934a 3931  reclem2pr 3951  recexsrlem 4006  map2psrpr 4014  supsrlem2 4020  ltsor 4055  posex 4422  nnleltp1t 4448  nnsub 4450  creur 4532  creui 4533  uzind 4603  sqr0 4730  ruclem33 4917  ruclem35 4919  infxpidmlem7 4939  infunabs 4946  infcdaabs 4947  alephexp2 4956  normgt0t 5078  occllem4 5183  occllem6 5185  projlem2 5194  projlem8 5200  projlem13 5205  projlem15 5207  projlem24 5216  projlem25 5217  projlem26 5218  projlem29 5221  pjthlem4 5228  pjthlem7 5231  pjthlem10 5234  pjthlem11 5235  pjthlem12 5236  pjthlem14 5238  pjoc1 5268  shlej1 5349  chlejb1 5397  cmbr4 5510  pjjs 5585  pjnormss 5638  stge1 5679  stle0 5680  stles 5682  stadd 5687  stadd3 5689  strlem3a 5693  strlem5 5696  jplem1 5701  mdbr3 5729  mdbr4 5730

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org