Theorem jctild 535

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 26	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		jctild.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	jcad 522	1 ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anc2li  565  equvini  2485  2reu1  3845  frpoinsg  6345  ordunidif  6412  isofrlem  7346  dfwe2  7786  orduniorsuc  7839  tfisg  7863  poxp  8138  fnse  8143  ssenen  9163  dffi3  9416  fpwwe2lem12  10720  zmulcl  12738  rpneg  13147  rexuz3  15509  cau3lem  15515  climrlim2  15707  o1rlimmul  15779  iseralt  15845  gcdzeq  16718  isprm3  16851  vdwnnlem2  17167  chnccat  18793  ablfaclem3  20296  epttop  23320  lmcnp  23615  dfconn2  23730  txcnp  23932  cmphaushmeo  24112  isfild  24170  cnpflf2  24312  flimfnfcls  24340  alexsubALT  24363  fgcfil  25585  bcthlem5  25642  ivthlem2  25766  ivthlem3  25767  dvfsumrlim  26344  plypf1  26524  noetalem1  28091  noseqinds  28672  axeuclidlem  29533  usgr2wlkneq  30335  wwlksnredwwlkn0  30478  wwlksnextwrd  30479  clwlkclwwlklem2a1  30576  lnon0  31393  hstles  32826  mdsl1i  32916  atcveq0  32943  atcvat4i  32992  cdjreui  33027  issgon  34748  onvfowev  35878  connpconn  35979  outsideofrflx  36872  isbasisrelowllem1  38258  isbasisrelowllem2  38259  poimirlem3  38521  poimirlem29  38547  poimir  38551  heicant  38553  equivtotbnd  38692  ismtybndlem  38720  cvrat4  40480  linepsubN  40789  pmapsub  40805  osumcllem4N  40996  pexmidlem1N  41007  dochexmidlem1  42497  cantnfresb  44310  harval3  44523  clcnvlem  44608  relpfrlem  45921  iccpartimp  48468  sbgoldbwt  48844  sbgoldbst  48845  elsetrecslem  50761