Theorem jctird 568

Description: Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses

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

Assertion

Ref	Expression
jctird	⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Proof of Theorem jctird

Step	Hyp	Ref	Expression
1		jctird.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		jctird.2	. . 3 ⊢ (𝜑 → 𝜃)
3	2	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	1, 3	jcad 556	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 383

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

This theorem depends on definitions:  df-bi 197  df-an 385

This theorem is referenced by:  anc2ri  582  fnun  6158  fco  6219  mapdom2  8296  fisupg  8373  fiint  8402  dffi3  8502  fiinfg  8570  dfac2b  9143  dfac2OLD  9145  cflm  9264  cfslbn  9281  cardmin  9578  fpwwe2lem12  9655  fpwwe2lem13  9656  elfznelfzob  12768  modsumfzodifsn  12937  dvdsdivcl  15240  isprm5  15621  latjlej1  17266  latmlem1  17282  cnrest2  21292  cnpresti  21294  trufil  21915  stdbdxmet  22521  lgsdir  25256  elwwlks2  27088  orthin  28614  mdbr2  29464  dmdbr2  29471  mdsl2i  29490  atcvat4i  29565  mdsymlem3  29573  wzel  32075  ontgval  32736  poimirlem3  33725  poimirlem4  33726  poimirlem29  33751  poimir  33755  cmtbr4N  35045  cvrat4  35232  cdlemblem  35582  elpglem2  42968