Theorem expcomd 422

Description: Deduction form of expcom 419. (Contributed by Alan Sare, 22-Jul-2012.)

Hypothesis

Ref	Expression
expcomd.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
expcomd	⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

Proof of Theorem expcomd

Step	Hyp	Ref	Expression
1		expcomd.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 421	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 87	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:  ancomsd  471  simplbi2comt  507  ralrimdva  3163  reupick  4275  pwssun  5543  ordelord  6377  tz7.7  6381  onelssex  6405  poxp  8129  smores2  8346  smoiun  8353  smogt  8359  tz7.49  8439  omsmolem  8650  mapxpen  9146  fodomfir  9303  f1dmvrnfibi  9314  suplub2  9437  epfrs  9716  r1sdom  9764  rankr1ai  9788  hfelhfOLD  9897  ficardom  10023  cardsdomel  10036  dfac5lem5  10187  cfsmolem  10329  cfcoflem  10331  axdc3lem2  10510  zorn2lem7  10561  genpn0  11069  reclem2pr  11114  supsrlem  11177  ltletr  11383  fzind  12778  rpneg  13135  xrltletr  13267  iccid  13502  ssfzoulel  13875  ssfzo12bi  13876  pfxccatin12lem2  14860  swrdccat  14864  repsdf2  14909  repswswrd  14915  cshwcsh2id  14959  o1rlimmul  15766  dvdsabseq  16463  divalgb  16554  bezoutlem3  16694  cncongr1  16822  ncoprmlnprm  16884  difsqpwdvds  17045  lss1d  21218  pf1ind  22653  chfacfisf  23152  chfacfisfcpmat  23153  cayleyhamilton1  23190  txlm  23947  fmfnfmlem1  24253  blsscls2  24803  metcnpi3  24845  bcmono  27586  lestr  28101  elreno2  28863  upgrewlkle2  30169  redwlk  30233  crctcshwlkn0lem5  30385  wwlksnextwrd  30468  clwwlknonex2lem2  30681  ocnel  31882  atcvat2i  32971  atcvat4i  32981  rankfilimb  35707  trssfir1om  35716  trssfir1omregs  35777  dfon2lem5  36519  cgrxfr  36790  colinearxfr  36810  isbasisrelowllem1  38246  isbasisrelowllem2  38247  finxpreclem6  38287  seqpo  38649  atlatle  40345  cvrexchlem  40444  cvrat2  40454  cvrat4  40468  pmapjoin  40877  onfrALTlem2  45488  onfrALTlem2VD  45830  eluzge0nn0  48326  elfz2z  48329  iccpartiltu  48448  iccpartigtl  48449  iccpartlt  48450  lighneal  48640  bgoldbtbnd  48851  tgoldbach  48859  cznnring  49303  ply1mulgsumlem2  49443  itsclc0  49827