Theorem jctild 530

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 517	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 208  df-an 397

This theorem is referenced by:  anc2li  560  equvini  2463  2reu1  3836  frpoinsg  6301  ordunidif  6367  isofrlem  7291  dfwe2  7724  orduniorsuc  7777  tfisg  7801  poxp  8075  fnse  8080  ssenen  9086  dffi3  9341  fpwwe2lem12  10563  zmulcl  12574  rpneg  12974  rexuz3  15309  cau3lem  15315  climrlim2  15507  o1rlimmul  15579  iseralt  15645  gcdzeq  16519  isprm3  16650  vdwnnlem2  16965  chnccat  18590  ablfaclem3  20062  epttop  22999  lmcnp  23294  dfconn2  23409  txcnp  23610  cmphaushmeo  23790  isfild  23848  cnpflf2  23990  flimfnfcls  24018  alexsubALT  24041  fgcfil  25263  bcthlem5  25320  ivthlem2  25444  ivthlem3  25445  dvfsumrlim  26023  plypf1  26202  noetalem1  27730  noseqinds  28310  axeuclidlem  29056  usgr2wlkneq  29849  wwlksnredwwlkn0  29989  wwlksnextwrd  29990  clwlkclwwlklem2a1  30087  lnon0  30894  hstles  32327  mdsl1i  32417  atcveq0  32444  atcvat4i  32493  cdjreui  32528  issgon  34314  connpconn  35470  outsideofrflx  36362  isbasisrelowllem1  37724  isbasisrelowllem2  37725  poimirlem3  37997  poimirlem29  38023  poimir  38027  heicant  38029  equivtotbnd  38152  ismtybndlem  38180  cvrat4  39942  linepsubN  40251  pmapsub  40267  osumcllem4N  40458  pexmidlem1N  40469  dochexmidlem1  41959  cantnfresb  43776  harval3  43989  clcnvlem  44074  relpfrlem  45404  iccpartimp  47899  sbgoldbwt  48275  sbgoldbst  48276  elsetrecslem  50196