Theorem 3impia 1117

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis

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

Assertion

Ref	Expression
3impia	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	expimpd 453	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1116	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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  df-3an 1088

This theorem is referenced by:  mopick2  2634  ceqsalt  3471  3gencl  3481  vtoclgft  3506  vtoclegft  3540  rspc6v  3594  mob2  3670  moi  3673  reupick3  4279  disjne  4404  elpr2elpr  4822  disji2  5079  disji  5080  tz7.2  5604  sofld  6142  ordintdif  6365  funopg  6523  fvun1  6922  fvopab6  6972  fveqressseq  7021  fvcofneq  7035  fprg  7097  isores3  7278  ovmpt4g  7502  ovmpos  7503  ov2gf  7504  ofrval  7631  sorpssuni  7674  sorpssint  7675  poxp  8067  poseq  8097  suppss2  8139  frrlem12  8236  smoel  8289  smoord  8294  smogt  8296  oaass  8485  oewordi  8515  oeoalem  8520  oeoelem  8522  nnawordi  8545  nnaass  8546  naddssim  8609  qsel  8729  xpdom3  8999  onsdominel  9050  mapdom3  9073  sdomdomtrfi  9121  domsdomtrfi  9122  php  9127  onomeneq  9134  fisseneq  9158  fodomfir  9223  cantnflem1  9590  ttrclss  9621  cfslbn  10169  cfsmolem  10172  cfcoflem  10174  infpssrlem4  10208  fin23lem7  10218  fin23lem25  10226  isf34lem7  10281  hsmexlem2  10329  axcc3  10340  axdc4lem  10357  tskss  10660  gruss  10698  gruurn  10700  gruiun  10701  gruel  10705  gruen  10714  grudomon  10719  grothac  10732  axpre-sup  11071  axsup  11199  addn0nid  11548  letrp1  11976  p1le  11977  lemul1a  11986  infrelb  12118  zextle  12556  zextlt  12557  btwnnz  12559  gtndiv  12560  uzind2  12576  fzind  12581  zsupss  12841  xrltne  13068  lemaxle  13101  qbtwnre  13105  qbtwnxr  13106  xlemul1a  13194  icogelb  13303  iccleub  13308  iccsplit  13392  uzsubsubfz  13453  elfz0fzfz0  13540  difelfznle  13549  fvffz0  13553  elfzo0le  13610  fzonmapblen  13615  fzofzim  13616  ceile  13760  modadd1  13819  muladdmodid  13824  modmul1  13838  modirr  13856  fsuppmapnn0fiub0  13907  expcl2lem  13987  expclzlem  13997  expnegz  14010  leexp2r  14088  bcval4  14221  bccmpl  14223  hashbnd  14250  hashunsnggt  14308  hashgt23el  14338  hashfundm  14356  elovmpowrd  14472  ccatval2  14492  ccatrcl1  14509  wrdl1s1  14529  ccat2s1fvw  14553  swrdsb0eq  14578  swrdccatin1  14639  pfxccatpfx2  14651  repswswrd  14698  cshwcsh2id  14742  absexpz  15219  climbdd  15586  iseraltlem2  15597  binomfallfac  15955  dvdsle  16228  divalgb  16322  ndvdssub  16327  dvdsgcd  16462  dfgcd2  16464  rplpwr  16476  nn0rppwr  16479  nn0expgcd  16482  lcmgcdlem  16524  lcmfunsn  16562  coprmdvds1  16570  qredeq  16575  2mulprm  16611  prmdvdsexpr  16635  nnnn0modprm0  16725  prm23ge5  16734  pcexp  16778  difsqpwdvds  16806  prmpwdvds  16823  ramcl  16948  cshwshashlem3  17016  cshwrepswhash1  17021  elrestr  17339  mreintcl  17505  mremre  17514  mrieqv2d  17553  initoeu2lem1  17929  funcestrcsetclem9  18062  funcsetcestrclem9  18077  prstr  18213  drsdirfi  18219  latnlej  18370  latnlej2  18373  acsdrsel  18457  acsdrscl  18460  mrelatglb  18474  mrelatlub  18476  isnmgm  18560  grpasscan1  18922  grpinvnz  18931  mulgneg2  19029  gsmsymgrfix  19348  f1omvdco2  19368  symggen  19390  odcl2  19485  odhash3  19496  lsmss1  19585  lsmss2  19587  efgred  19668  efgcpbl  19676  ablfacrp  19988  ablfac1eu  19995  ablfaclem3  20009  omndadd  20048  ogrpaddlt  20058  dvdsrmul1  20296  dvdsunit  20306  irredmul  20356  c0snmgmhm  20389  lmodlema  20807  psgnodpmr  21536  phlssphl  21605  lindsss  21770  lindfmm  21773  ply1scln0  22225  dmatelnd  22431  mdetdiaglem  22533  mdet0  22541  mdetunilem7  22553  slesolinv  22615  cramerimplem3  22620  cpmatpmat  22645  m2cpminvid2lem  22689  chfacfscmul0  22793  chfacfpmmul0  22797  riinopn  22843  clsndisj  23010  cnpf2  23185  hausnei2  23288  cmpcov  23324  cmpfii  23344  unconn  23364  t1connperf  23371  nrmr0reg  23684  fbfinnfr  23776  filuni  23820  alexsubALT  23986  tmdgsum  24030  cuspcvg  24235  mopni  24427  isngp4  24547  metdsre  24789  iimulcl  24880  phtpc01  24942  clmmulg  25048  cfilucfil4  25268  bcthlem5  25275  bcth  25276  bcth3  25278  itg1le  25661  itg2le  25687  bddmulibl  25787  bddiblnc  25790  dvnres  25880  cpnord  25884  dvnfre  25903  deg1ge  26050  dgr1term  26212  aaliou3lem2  26298  sincosq1lem  26453  cxpge0  26639  cxpmul2  26645  logrec  26720  logbgcd1irr  26751  sqfpc  27094  bcmono  27235  gausslemma2dlem1a  27323  gausslemma2dlem2  27325  gausslemma2dlem4  27327  2lgsoddprmlem3  27372  pntrmax  27522  qabvexp  27584  ostth2lem2  27592  nosepon  27624  nolesgn2o  27630  nogesgn1o  27632  nosepnelem  27638  nosepne  27639  nosepdmlem  27642  nosepdm  27643  nodenselem8  27650  noresle  27656  noetasuplem4  27695  noetainflem4  27699  scutbdaylt  27779  eqscut3  27785  addsuniflem  27964  ssltmul1  28106  precsexlem6  28170  precsexlem7  28171  precsexlem11  28175  sltonold  28218  onnolt  28223  n0sfincut  28302  expadds  28378  ax5seglem4  28931  axeuclidlem  28961  uhgredgrnv  29129  usgredg4  29216  nbuhgr2vtx1edgblem  29350  vtxduhgr0e  29478  vtxduhgr0nedg  29492  rusgrpropnb  29583  uspgr2wlkeqi  29647  redwlklem  29669  lfgrwlkprop  29685  2pthnloop  29730  spthonepeq  29751  pthdlem2lem  29766  crctcshwlkn0lem3  29811  crctcshwlkn0lem5  29813  crctcshwlkn0lem7  29815  crctcshwlkn0  29820  wlkiswwlks1  29866  wlkiswwlks2  29874  wlkiswwlksupgr2  29876  wwlksnext  29892  wwlksnextproplem2  29909  wspthsnonn0vne  29916  2pthon3v  29942  rusgrnumwwlk  29977  erclwwlkeqlen  30020  erclwwlksym  30022  erclwwlktr  30023  erclwwlkneqlen  30069  erclwwlknsym  30071  erclwwlkntr  30072  uhgr3cyclex  30183  upgreupthseg  30210  eupth2lem3lem4  30232  eucrctshift  30244  4cycl2vnunb  30291  nvs  30664  nvtri  30671  nmlno0  30796  nmlnoubi  30797  ubth  30874  hlipgt0  30915  ocnel  31299  elspansn2  31568  elspansn3  31573  normcan  31577  pjoml2  31612  lecm  31618  osum  31646  nmbdfnlb  32051  leopmul  32135  hstpyth  32230  cvnbtwn  32287  ssmd1  32312  ssmd2  32313  ssdmd1  32314  ssdmd2  32315  cvmd  32337  cvdmd  32338  superpos  32355  disji2f  32578  disjif  32579  disjif2  32582  preiman0  32715  padct  32725  ffs2  32734  bcm1n  32803  sgn3da  32843  s2f1  32955  archiabl  33208  slmdlema  33213  lbslsat  33701  eulerpartlemb  34453  fisshasheq  35231  cvmsdisj  35386  cvmlift2lem12  35430  satfrel  35483  satfrnmapom  35486  fmlasuc  35502  satffun  35525  satef  35532  sategoelfv  35536  lineintmo  36273  nn0prpwlem  36438  nn0prpw  36439  neibastop2lem  36476  lindsadd  37726  areacirc  37826  incsequz  37861  mettrifi  37870  ismtybnd  37920  heiborlem1  37924  rngoisocnv  38094  risci  38100  eqvrelqsel  38785  lfl1  39242  lkrlsp2  39275  omlfh3N  39431  cvrnbtwn  39443  cvrnbtwn2  39447  cvrnbtwn4  39451  cvlexch3  39504  cvlexch4N  39505  cvlatexchb1  39506  2llnne2N  39580  atcvrj0  39600  cvrat2  39601  ps-1  39649  3atlem5  39659  islln2a  39689  lplnriaN  39722  lplnribN  39723  llncvrlpln2  39729  lplncvrlvol2  39787  psubatN  39927  pmapglb2N  39943  pmapglb2xN  39944  2llnma1b  39958  paddasslem17  40008  pmod2iN  40021  pmodl42N  40023  hlmod1i  40028  atmod1i1  40029  atmod1i2  40031  llnmod1i2  40032  pclcmpatN  40073  osumcllem8N  40135  pexmidlem3N  40144  pl42lem4N  40154  4atexlem7  40247  ltrnnid  40308  cdlemc4  40366  cdleme32a  40613  cdlemeg46gfre  40704  cdlemf2  40734  cdlemg4c  40784  trlcoat  40895  tendovalco  40937  tendoeq2  40946  cdlemk36  41085  diael  41215  diatrl  41216  dicelval1stN  41360  dicelval2nd  41361  dihlspsnat  41505  dochkr1  41650  lcfrlem9  41722  mapdh8e  41956  hdmapval0  42005  hgmapval0  42064  nnadddir  42440  dvdsexpnn0  42504  incssnn0  42868  pell14qrexpcl  43024  pell14qrgap  43032  congadd  43123  acongsym  43133  acongtr  43135  dvdsacongtr  43141  jm2.19lem3  43148  jm2.19lem4  43149  jm2.26lem3  43158  onexlimgt  43400  nadd2rabex  43543  ismnushort  44458  bi13impia  44646  3impcombi  44973  ioogtlb  45657  iocgtlb  45664  iocleub  45665  icoltub  45670  iooltub  45672  limclner  45811  limsupre3lem  45892  climuzlem  45903  fsupdm  47002  finfdm  47006  elfzelfzlble  47483  subsubelfzo0  47488  m1modnep2mod  47514  m1modmmod  47520  modlt0b  47525  mod2addne  47526  iccpartigtl  47585  sqrtpwpw2p  47700  fmtnoprmfac1lem  47726  fmtno4prmfac  47734  evenltle  47879  even3prm2  47881  wtgoldbnnsum4prm  47964  bgoldbnnsum3prm  47966  bgoldbtbndlem1  47967  bgoldbtbndlem3  47969  bgoldbtbndlem4  47970  bgoldbtbnd  47971  uhgrimisgrgriclem  48092  isubgr3stgrlem7  48134  clnbgr3stgrgrlic  48182  gpgedg2iv  48229  pgnbgreunbgrlem3  48280  pgnbgreunbgrlem6  48286  upgrwlkupwlk  48302  funcringcsetcALTV2lem9  48460  funcringcsetclem9ALTV  48483  lincscmcl  48594  lindslinindimp2lem4  48623  lincresunit2  48640  lincresunit3  48643  elfzolborelfzop1  48681  rege1logbzge0  48721  fllog2  48730  dignn0ldlem  48764  rrx2pnecoorneor  48877  rrx2plord2  48884  rrx2linest  48904  ipolub  49149  ipoglb  49152