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  6604  fcof  6683  brinxper  8662  mapdom2  9074  fisupg  9186  fiint  9225  dffi3  9332  fiinfg  9402  dfac2b  10039  nnadju  10106  cflm  10158  cfslbn  10175  cardmin  10472  fpwwe2lem11  10550  fpwwe2lem12  10551  elfznelfzob  13688  modsumfzodifsn  13865  dvdsdivcl  16241  isprm5  16632  latjlej1  18374  latmlem1  18390  chnccat  18547  cnrest2  23228  cnpresti  23230  trufil  23852  stdbdxmet  24457  lgsdir  27297  elwwlks2  29991  orthin  31470  mdbr2  32320  dmdbr2  32327  mdsl2i  32346  atcvat4i  32421  mdsymlem3  32429  tz9.1regs  35239  wzel  35965  ontgval  36574  poimirlem3  37763  poimirlem4  37764  poimirlem29  37789  poimir  37793  cmtbr4N  39454  cvrat4  39642  cdlemblem  39992  negexpidd  42866  3cubeslem1  42868  tfsconcatb0  43528  ensucne0OLD  43713  itschlc0xyqsol  48955  elpglem2  49899