Theorem jctird 527

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  anc2ri  557  pm5.31  829  fnun  6660  fcof  6737  fcoOLD  6739  mapdom2  9144  fisupg  9287  fiint  9320  dffi3  9422  fiinfg  9490  dfac2b  10121  nnadju  10188  cflm  10241  cfslbn  10258  cardmin  10555  fpwwe2lem11  10632  fpwwe2lem12  10633  elfznelfzob  13734  modsumfzodifsn  13905  dvdsdivcl  16255  isprm5  16640  latjlej1  18402  latmlem1  18418  cnrest2  22781  cnpresti  22783  trufil  23405  stdbdxmet  24015  lgsdir  26824  elwwlks2  29209  orthin  30686  mdbr2  31536  dmdbr2  31543  mdsl2i  31562  atcvat4i  31637  mdsymlem3  31645  wzel  34784  ontgval  35304  poimirlem3  36479  poimirlem4  36480  poimirlem29  36505  poimir  36509  cmtbr4N  38113  cvrat4  38302  cdlemblem  38652  negexpidd  41405  3cubeslem1  41407  tfsconcatb0  42079  ensucne0OLD  42266  itschlc0xyqsol  47406  elpglem2  47710