Theorem jctild 529

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anc2li  559  equvini  2466  2reu1  3826  ordunidif  6207  isofrlem  7072  dfwe2  7476  orduniorsuc  7525  poxp  7805  fnse  7810  ssenen  8675  dffi3  8879  fpwwe2lem13  10053  zmulcl  12019  rpneg  12409  rexuz3  14700  cau3lem  14706  climrlim2  14896  o1rlimmul  14967  iseralt  15033  gcdzeq  15892  isprm3  16017  vdwnnlem2  16322  ablfaclem3  19202  epttop  21614  lmcnp  21909  dfconn2  22024  txcnp  22225  cmphaushmeo  22405  isfild  22463  cnpflf2  22605  flimfnfcls  22633  alexsubALT  22656  fgcfil  23875  bcthlem5  23932  ivthlem2  24056  ivthlem3  24057  dvfsumrlim  24634  plypf1  24809  axeuclidlem  26756  usgr2wlkneq  27545  wwlksnredwwlkn0  27682  wwlksnextwrd  27683  clwlkclwwlklem2a1  27777  lnon0  28581  hstles  30014  mdsl1i  30104  atcveq0  30131  atcvat4i  30180  cdjreui  30215  issgon  31492  connpconn  32595  tfisg  33168  frpoinsg  33194  frmin  33197  outsideofrflx  33701  isbasisrelowllem1  34772  isbasisrelowllem2  34773  poimirlem3  35060  poimirlem29  35086  poimir  35090  heicant  35092  equivtotbnd  35216  ismtybndlem  35244  cvrat4  36739  linepsubN  37048  pmapsub  37064  osumcllem4N  37255  pexmidlem1N  37266  dochexmidlem1  38756  harval3  40244  clcnvlem  40323  iccpartimp  43934  sbgoldbwt  44295  sbgoldbst  44296  elsetrecslem  45228