Theorem jctild 525

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

Hypotheses

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

Assertion

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

Proof of Theorem jctild

Step	Hyp	Ref	Expression
1		jctild.2	. . 3 ⊢ (𝜑 → 𝜃)
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		jctild.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 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:  anc2li  555  equvini  2455  2reu1  3843  frpoinsg  6285  ordunidif  6351  isofrlem  7269  dfwe2  7702  orduniorsuc  7755  tfisg  7779  poxp  8053  fnse  8058  ssenen  9059  dffi3  9310  fpwwe2lem12  10528  zmulcl  12516  rpneg  12919  rexuz3  15251  cau3lem  15257  climrlim2  15449  o1rlimmul  15521  iseralt  15587  gcdzeq  16458  isprm3  16589  vdwnnlem2  16903  chnccat  18527  ablfaclem3  19996  epttop  22919  lmcnp  23214  dfconn2  23329  txcnp  23530  cmphaushmeo  23710  isfild  23768  cnpflf2  23910  flimfnfcls  23938  alexsubALT  23961  fgcfil  25193  bcthlem5  25250  ivthlem2  25375  ivthlem3  25376  dvfsumrlim  25960  plypf1  26139  noetalem1  27675  noseqinds  28218  axeuclidlem  28935  usgr2wlkneq  29729  wwlksnredwwlkn0  29869  wwlksnextwrd  29870  clwlkclwwlklem2a1  29964  lnon0  30770  hstles  32203  mdsl1i  32293  atcveq0  32320  atcvat4i  32369  cdjreui  32404  issgon  34128  connpconn  35271  outsideofrflx  36161  isbasisrelowllem1  37389  isbasisrelowllem2  37390  poimirlem3  37663  poimirlem29  37689  poimir  37693  heicant  37695  equivtotbnd  37818  ismtybndlem  37846  cvrat4  39482  linepsubN  39791  pmapsub  39807  osumcllem4N  39998  pexmidlem1N  40009  dochexmidlem1  41499  cantnfresb  43357  harval3  43571  clcnvlem  43656  relpfrlem  44986  iccpartimp  47448  sbgoldbwt  47808  sbgoldbst  47809  elsetrecslem  49731