Theorem jctir 306

Description: Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.)

Hypotheses

Ref	Expression
jctil.1	⊢ (𝜑 → 𝜓)
jctil.2	⊢ 𝜒

Assertion

Ref	Expression
jctir	⊢ (𝜑 → (𝜓 ∧ 𝜒))

Proof of Theorem jctir

Step	Hyp	Ref	Expression
1		jctil.1	. 2 ⊢ (𝜑 → 𝜓)
2		jctil.2	. . 3 ⊢ 𝜒
3	2	a1i 9	. 2 ⊢ (𝜑 → 𝜒)
4	1, 3	jca 300	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  jctr  308  equvini  1685  funtp  5023  foimacnv  5222  respreima  5375  fpr  5424  dmtpos  5956  ssdomg  6428  exmidfodomrlemim  6748  archnqq  6897  recexgt0sr  7240  ige2m2fzo  9512  climeu  10523  algcvgblem  10825  qredeu  10873  qnumdencoprm  10965  qeqnumdivden  10966  exmidsbthrlem  11268