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  6595  fcof  6674  brinxper  8651  mapdom2  9061  fisupg  9172  fiint  9211  dffi3  9315  fiinfg  9385  dfac2b  10022  nnadju  10089  cflm  10141  cfslbn  10158  cardmin  10455  fpwwe2lem11  10532  fpwwe2lem12  10533  elfznelfzob  13674  modsumfzodifsn  13851  dvdsdivcl  16227  isprm5  16618  latjlej1  18359  latmlem1  18375  chnccat  18532  cnrest2  23201  cnpresti  23203  trufil  23825  stdbdxmet  24430  lgsdir  27270  elwwlks2  29947  orthin  31426  mdbr2  32276  dmdbr2  32283  mdsl2i  32302  atcvat4i  32377  mdsymlem3  32385  tz9.1regs  35130  wzel  35866  ontgval  36475  poimirlem3  37673  poimirlem4  37674  poimirlem29  37699  poimir  37703  cmtbr4N  39364  cvrat4  39552  cdlemblem  39902  negexpidd  42785  3cubeslem1  42787  tfsconcatb0  43447  ensucne0OLD  43633  itschlc0xyqsol  48878  elpglem2  49823