Theorem jctird 526

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 512	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anc2ri  556  pm5.31  830  fnun  6652  fcof  6729  brinxper  8748  mapdom2  9162  fisupg  9296  fiint  9338  fiintOLD  9339  dffi3  9443  fiinfg  9513  dfac2b  10145  nnadju  10212  cflm  10264  cfslbn  10281  cardmin  10578  fpwwe2lem11  10655  fpwwe2lem12  10656  elfznelfzob  13789  modsumfzodifsn  13962  dvdsdivcl  16335  isprm5  16726  latjlej1  18463  latmlem1  18479  cnrest2  23224  cnpresti  23226  trufil  23848  stdbdxmet  24454  lgsdir  27295  elwwlks2  29948  orthin  31427  mdbr2  32277  dmdbr2  32284  mdsl2i  32303  atcvat4i  32378  mdsymlem3  32386  wzel  35842  ontgval  36449  poimirlem3  37647  poimirlem4  37648  poimirlem29  37673  poimir  37677  cmtbr4N  39273  cvrat4  39462  cdlemblem  39812  negexpidd  42705  3cubeslem1  42707  tfsconcatb0  43368  ensucne0OLD  43554  itschlc0xyqsol  48747  elpglem2  49576